Structures · Other
MulAction.IsMinimal
An action of a monoid M on a topological space is called minimal if the M-orbit of every
point x : α is dense.
- Defined in
- Mathlib.Dynamics.Minimal
- Shape
- 2 explicit arguments · adds dense_orbit
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by16
- IsOpen.exists_smul_mem
- MulAction.dense_orbit
- dense_of_nonempty_smul_invariant
- IsOpen.iUnion_smul
- MeasureTheory.measure_isOpen_pos_of_smulInvariant_of_compact_ne_zero
- MeasureTheory.measure_isOpen_pos_of_smulInvariant_of_ne_zero
- MeasureTheory.measure_pos_iff_nonempty_of_smulInvariant
- MulAction.IsMinimal.dense_orbit
- eq_empty_or_univ_of_smul_invariant_closed
- denseRange_smul
- IsCompact.exists_finite_cover_smul
- MeasureTheory.measure_eq_zero_iff_eq_empty_of_smulInvariant
- IsOpen.iUnion_preimage_smul
- MeasureTheory.isLocallyFiniteMeasure_of_smulInvariant
- ErgodicSMul.trans_isMinimal
- MulAction.isTopologicallyTransitive_of_isMinimal
Ancestors0
No ancestors.