eq_empty_or_univ_of_smul_invariant_closed

English

Let α be acted on by M with a minimal action. If s ⊆ α is closed and invariant under the action (c • s ⊆ s for all c ∈ M), then either s is empty or s is all of α.

Русский

Пусть M действует минимально на α. Если s ⊆ α замкнуто и инвариантно по отношению к действию (для всех c ∈ M выполняется c•s ⊆ s), то либо s пусто, либо s равно всему α.

LaTeX

$$$$s=\varnothing \quad\text{или}\quad s=\mathrm{univ}.$$$$

Lean4

@[to_additive]
theorem eq_empty_or_univ_of_smul_invariant_closed [IsMinimal M α] {s : Set α} (hs : IsClosed s)
    (hsmul : ∀ c : M, c • s ⊆ s) : s = ∅ ∨ s = univ :=
  s.eq_empty_or_nonempty.imp_right fun hne ↦ hs.closure_eq ▸ (dense_of_nonempty_smul_invariant M hne hsmul).closure_eq

Похожие утверждения