Theorems · Theorem · dynamical systems

IsOpen.exists_vadd_mem

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

AddMonoidTopologicalSpaceAddActionAddAction.IsMinimal