English
A continuous constant-smul action of a group G on α is minimal if and only if every closed invariant subset is either empty or the whole space.
Русский
Пусть действие группы G на α с непрерывным постоянным умножением является минимальным тогда и только тогда, когда каждое замкнутое инвариантное подмножество пусто или является всем пространством.
LaTeX
$$$$\text{IsMinimal}(G,\alpha) \iff \forall s\subseteq \alpha,\ \text{IsClosed}(s) \to (\forall c:\,G, c\cdot s\subseteq s) \to (s=\varnothing \lor s=\alpha).$$$$
Lean4
@[to_additive]
theorem isMinimal_iff_isClosed_smul_invariant [ContinuousConstSMul M α] :
IsMinimal M α ↔ ∀ s : Set α, IsClosed s → (∀ c : M, c • s ⊆ s) → s = ∅ ∨ s = univ :=
by
constructor
· intro _ _
exact eq_empty_or_univ_of_smul_invariant_closed M
refine fun H ↦ ⟨fun _ ↦ dense_iff_closure_eq.2 <| (H _ ?_ ?_).resolve_left ?_⟩
exacts [isClosed_closure, fun _ ↦ smul_closure_orbit_subset _ _, (nonempty_orbit _).closure.ne_empty]
