# Minimal action of a group #

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 AddAction.IsMinimal (M : Type u_1) (α : Type u_2) [] [] [] :

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

• dense_orbit : ∀ (x : α), Dense ()
Instances
theorem AddAction.IsMinimal.dense_orbit {M : Type u_1} {α : Type u_2} [] [] [] [self : ] (x : α) :
class MulAction.IsMinimal (M : Type u_1) (α : Type u_2) [] [] [] :

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

• dense_orbit : ∀ (x : α), Dense ()
Instances
theorem MulAction.IsMinimal.dense_orbit {M : Type u_1} {α : Type u_2} [] [] [] [self : ] (x : α) :
theorem AddAction.dense_orbit (M : Type u_1) {α : Type u_3} [] [] [] [] (x : α) :
theorem MulAction.dense_orbit (M : Type u_1) {α : Type u_3} [] [] [] [] (x : α) :
theorem denseRange_vadd (M : Type u_1) {α : Type u_3} [] [] [] [] (x : α) :
DenseRange fun (c : M) => c +ᵥ x
theorem denseRange_smul (M : Type u_1) {α : Type u_3} [] [] [] [] (x : α) :
DenseRange fun (c : M) => c x
@[instance 100]
instance AddAction.isMinimal_of_pretransitive (M : Type u_1) {α : Type u_3} [] [] [] :
Equations
• =
@[instance 100]
instance MulAction.isMinimal_of_pretransitive (M : Type u_1) {α : Type u_3} [] [] [] :
Equations
• =
theorem IsOpen.exists_vadd_mem (M : Type u_1) {α : Type u_3} [] [] [] [] (x : α) {U : Set α} (hUo : ) (hne : U.Nonempty) :
∃ (c : M), c +ᵥ x U
theorem IsOpen.exists_smul_mem (M : Type u_1) {α : Type u_3} [] [] [] [] (x : α) {U : Set α} (hUo : ) (hne : U.Nonempty) :
∃ (c : M), c x U
theorem IsOpen.iUnion_preimage_vadd (M : Type u_1) {α : Type u_3} [] [] [] [] {U : Set α} (hUo : ) (hne : U.Nonempty) :
⋃ (c : M), (fun (x : α) => c +ᵥ x) ⁻¹' U = Set.univ
theorem IsOpen.iUnion_preimage_smul (M : Type u_1) {α : Type u_3} [] [] [] [] {U : Set α} (hUo : ) (hne : U.Nonempty) :
⋃ (c : M), (fun (x : α) => c x) ⁻¹' U = Set.univ
abbrev IsOpen.iUnion_vadd.match_1 (G : Type u_1) {α : Type u_2} [] [] {U : Set α} (x : α) (motive : (∃ (c : G), c +ᵥ x U)Prop) :
∀ (x_1 : ∃ (c : G), c +ᵥ x U), (∀ (g : G) (hg : g +ᵥ x U), motive )motive x_1
Equations
• =
Instances For
theorem IsOpen.iUnion_vadd (G : Type u_2) {α : Type u_3} [] [] [] [] {U : Set α} (hUo : ) (hne : U.Nonempty) :
⋃ (g : G), g +ᵥ U = Set.univ
theorem IsOpen.iUnion_smul (G : Type u_2) {α : Type u_3} [] [] [] [] {U : Set α} (hUo : ) (hne : U.Nonempty) :
⋃ (g : G), g U = Set.univ
theorem IsCompact.exists_finite_cover_vadd (G : Type u_2) {α : Type u_3} [] [] [] [] [] {K : Set α} {U : Set α} (hK : ) (hUo : ) (hne : U.Nonempty) :
∃ (I : ), K gI, g +ᵥ U
theorem IsCompact.exists_finite_cover_smul (G : Type u_2) {α : Type u_3} [] [] [] [] [] {K : Set α} {U : Set α} (hK : ) (hUo : ) (hne : U.Nonempty) :
∃ (I : ), K gI, g U
theorem dense_of_nonempty_vadd_invariant (M : Type u_1) {α : Type u_3} [] [] [] [] {s : Set α} (hne : s.Nonempty) (hsmul : ∀ (c : M), c +ᵥ s s) :
abbrev dense_of_nonempty_vadd_invariant.match_1 {α : Type u_1} {s : Set α} (motive : s.NonemptyProp) :
∀ (hne : s.Nonempty), (∀ (x : α) (hx : x s), motive )motive hne
Equations
• =
Instances For
theorem dense_of_nonempty_smul_invariant (M : Type u_1) {α : Type u_3} [] [] [] [] {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} [] [] [] [] {s : Set α} (hs : ) (hsmul : ∀ (c : M), c +ᵥ s s) :
s = s = Set.univ
theorem eq_empty_or_univ_of_smul_invariant_closed (M : Type u_1) {α : Type u_3} [] [] [] [] {s : Set α} (hs : ) (hsmul : ∀ (c : M), c s s) :
s = s = Set.univ
theorem isMinimal_iff_closed_vadd_invariant (M : Type u_1) {α : Type u_3} [] [] [] [] :
∀ (s : Set α), (∀ (c : M), c +ᵥ s s)s = s = Set.univ
theorem isMinimal_iff_closed_smul_invariant (M : Type u_1) {α : Type u_3} [] [] [] [] :
∀ (s : Set α), (∀ (c : M), c s s)s = s = Set.univ