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⟩)