Theorems · Inductive type · dynamical systems

AddAction.IsTopologicallyTransitive

(M : Type u_1) → (α : Type u_2) → [inst : AddMonoid M] → [TopologicalSpace α] → [AddAction M α] → Prop

An action of an additive monoid M on a topological space α is called topologically transitive if for any pair of nonempty open sets U and V in α there exists an m : M such that (m +ᵥ U) ∩ V is nonempty.

Defined in

Mathlib.Dynamics.Transitive

Cited by

8 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

AddMonoidTopologicalSpaceAddAction