Theorems · Theorem · dynamical systems

IsOpen.exists_smul_mem

∀ (M : Type u_1) {α : Type u_3} [inst : Monoid M] [inst_1 : TopologicalSpace α] [inst_2 : MulAction M α]
  [MulAction.IsMinimal M α] (x : α) {U : Set α}, IsOpen U → U.Nonempty → ∃ c, c • x ∈ U

Defined in

Mathlib.Dynamics.Minimal

Cited by

3 results in Mathlib

Foundations

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

Assumes

MonoidTopologicalSpaceMulActionMulAction.IsMinimal