dynamics.minimal

Minimal action of a group #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define an action of a monoid M on a topological space α to be minimal if the M-orbit of every point x : α is dense. We also provide an additive version of this definition and prove some basic facts about minimal actions.

TODO #

• Define a minimal set of an action.

Tags #

group action, minimal

@[class]
structure add_action.is_minimal (M : Type u_1) (α : Type u_2) [add_monoid M] [ α] :
Prop

An action of an additive monoid M on a topological space is called minimal if the M-orbit of every point x : α is dense.

Instances of this typeclass
@[class]
structure mul_action.is_minimal (M : Type u_1) (α : Type u_2) [monoid M] [ α] :
Prop

An action of a monoid M on a topological space is called minimal if the M-orbit of every point x : α is dense.

Instances of this typeclass
theorem add_action.dense_orbit (M : Type u_1) {α : Type u_3} [add_monoid M] [ α] (x : α) :
theorem mul_action.dense_orbit (M : Type u_1) {α : Type u_3} [monoid M] [ α] (x : α) :
theorem dense_range_vadd (M : Type u_1) {α : Type u_3} [add_monoid M] [ α] (x : α) :
dense_range (λ (c : M), c +ᵥ x)
theorem dense_range_smul (M : Type u_1) {α : Type u_3} [monoid M] [ α] (x : α) :
dense_range (λ (c : M), c x)
@[protected, instance]
def add_action.is_minimal_of_pretransitive (M : Type u_1) {α : Type u_3} [add_monoid M] [ α]  :
@[protected, instance]
def mul_action.is_minimal_of_pretransitive (M : Type u_1) {α : Type u_3} [monoid M] [ α]  :
theorem is_open.exists_vadd_mem (M : Type u_1) {α : Type u_3} [add_monoid M] [ α] (x : α) {U : set α} (hUo : is_open U) (hne : U.nonempty) :
(c : M), c +ᵥ x U
theorem is_open.exists_smul_mem (M : Type u_1) {α : Type u_3} [monoid M] [ α] (x : α) {U : set α} (hUo : is_open U) (hne : U.nonempty) :
(c : M), c x U
theorem is_open.Union_preimage_smul (M : Type u_1) {α : Type u_3} [monoid M] [ α] {U : set α} (hUo : is_open U) (hne : U.nonempty) :
( (c : M), ⁻¹' U) = set.univ
theorem is_open.Union_preimage_vadd (M : Type u_1) {α : Type u_3} [add_monoid M] [ α] {U : set α} (hUo : is_open U) (hne : U.nonempty) :
( (c : M), ⁻¹' U) = set.univ
theorem is_open.Union_vadd (G : Type u_2) {α : Type u_3} [add_group G] [ α] {U : set α} (hUo : is_open U) (hne : U.nonempty) :
( (g : G), g +ᵥ U) = set.univ
theorem is_open.Union_smul (G : Type u_2) {α : Type u_3} [group G] [ α] {U : set α} (hUo : is_open U) (hne : U.nonempty) :
( (g : G), g U) = set.univ
theorem is_compact.exists_finite_cover_vadd (G : Type u_2) {α : Type u_3} [add_group G] [ α] {K U : set α} (hK : is_compact K) (hUo : is_open U) (hne : U.nonempty) :
(I : finset G), K (g : G) (H : g I), g +ᵥ U
theorem is_compact.exists_finite_cover_smul (G : Type u_2) {α : Type u_3} [group G] [ α] {K U : set α} (hK : is_compact K) (hUo : is_open U) (hne : U.nonempty) :
(I : finset G), K (g : G) (H : g I), g U
theorem dense_of_nonempty_smul_invariant (M : Type u_1) {α : Type u_3} [monoid M] [ α] {s : set α} (hne : s.nonempty) (hsmul : (c : M), c s s) :
theorem dense_of_nonempty_vadd_invariant (M : Type u_1) {α : Type u_3} [add_monoid M] [ α] {s : set α} (hne : s.nonempty) (hsmul : (c : M), c +ᵥ s s) :
theorem eq_empty_or_univ_of_vadd_invariant_closed (M : Type u_1) {α : Type u_3} [add_monoid M] [ α] {s : set α} (hs : is_closed s) (hsmul : (c : M), c +ᵥ s s) :
s =
theorem eq_empty_or_univ_of_smul_invariant_closed (M : Type u_1) {α : Type u_3} [monoid M] [ α] {s : set α} (hs : is_closed s) (hsmul : (c : M), c s s) :
s =
theorem is_minimal_iff_closed_smul_invariant (M : Type u_1) {α : Type u_3} [monoid M] [ α]  :
(s : set α), ( (c : M), c s s) s =
theorem is_minimal_iff_closed_vadd_invariant (M : Type u_1) {α : Type u_3} [add_monoid M] [ α]  :
(s : set α), ( (c : M), c +ᵥ s s) s =