Theorems · Theorem · dynamical systems

isMinimal_iff_isClosed_vadd_invariant

∀ (M : Type u_1) {α : Type u_3} [inst : AddMonoid M] [inst_1 : TopologicalSpace α] [inst_2 : AddAction M α]
  [ContinuousConstVAdd M α],
  AddAction.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

AddMonoidTopologicalSpaceAddActionContinuousConstVAdd