English
Equivalence between minimal action and a closed invariant-set dichotomy: continuous constant-smul action is minimal if and only if every closed invariant subset is either empty or the whole space.
Русский
Эквивалентность между минимальным действием и дихотомией для замкнутых инвариантных подмножеств: непрерывное константное умножение действует минимально тогда и только тогда, когда каждое замкнутое инвариантное множество либо пусто, либо равно всему пространству.
LaTeX
$$$$\text{IsMinimal}(M,\alpha) \iff \forall s,\ IsClosed(s) \to (\forall c:\,M, c\cdot s \subseteq s) \to (s=\varnothing \lor s=\alpha).$$$$
Lean4
/-- The ω-limit of a set `s` under `ϕ` with respect to a filter `f` is `⋂ u ∈ f, cl (ϕ u s)`. -/
def omegaLimit [TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s : Set α) : Set β :=
⋂ u ∈ f, closure (image2 ϕ u s)
