Theorems · Theorem · dynamical systems

isMinimal_iff_isClosed_smul_invariant

∀ (M : Type u_1) {α : Type u_3} [inst : Monoid M] [inst_1 : TopologicalSpace α] [inst_2 : MulAction M α]
  [ContinuousConstSMul M α],
  MulAction.IsMinimal M α ↔ ∀ (s : Set α), IsClosed s → (∀ (c : M), c • s ⊆ s) → s = ∅ ∨ s = Set.univ

Defined in

Mathlib.Dynamics.Minimal

Cited by

0 results in Mathlib

Foundations

Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MonoidTopologicalSpaceMulActionContinuousConstSMul