dense_of_nonempty_smul_invariant — Mathlib

English

If the action of G on α is minimal, then any nonempty set s that is invariant under the action (i.e., g·s ⊆ s for all g) is dense in α.

Русский

Если действие G на α минимально, то любое не пустое инвариантное множество s (такое что g·s ⊆ s для всех g) плотно в α.

LaTeX

$$$$\operatorname{Dense}(s)\quad\text{where } s\neq\varnothing\ \text{and}\ \forall g\in G:\ g\cdot s \subseteq s.$$$$

Lean4

@[to_additive]
theorem dense_of_nonempty_smul_invariant [IsMinimal M α] {s : Set α} (hne : s.Nonempty) (hsmul : ∀ c : M, c • s ⊆ s) :
    Dense s :=
  let ⟨x, hx⟩ := hne
  (MulAction.dense_orbit M x).mono (range_subset_iff.2 fun c ↦ hsmul c ⟨x, hx, rfl⟩)

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