Structures · Other
AddAction.IsMinimal
An action of an additive 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_vadd_mem
- AddAction.dense_orbit
- MeasureTheory.measure_isOpen_pos_of_vaddInvariant_of_compact_ne_zero
- eq_empty_or_univ_of_vadd_invariant_closed
- dense_of_nonempty_vadd_invariant
- denseRange_vadd
- MeasureTheory.measure_isOpen_pos_of_vaddInvariant_of_ne_zero
- MeasureTheory.measure_pos_iff_nonempty_of_vaddInvariant
- IsOpen.iUnion_vadd
- IsCompact.exists_finite_cover_vadd
- AddAction.IsMinimal.dense_orbit
- IsOpen.iUnion_preimage_vadd
- MeasureTheory.isLocallyFiniteMeasure_of_vaddInvariant
- MeasureTheory.measure_eq_zero_iff_eq_empty_of_vaddInvariant
- AddAction.isTopologicallyTransitive_of_isMinimal
- ErgodicVAdd.trans_isMinimal
Ancestors0
No ancestors.