IsOpen.exists_smul_mem
theorem IsOpen.exists_smul_mem :
∀ (M : Type u_1) {α : Type u_3} [inst : Monoid M] [inst_1 : TopologicalSpace α] [inst_2 : MulAction M α]
[inst_3 : MulAction.IsMinimal M α] (x : α) {U : Set α}, IsOpen U → U.Nonempty → ∃ c, c • x ∈ U
The theorem `IsOpen.exists_smul_mem` states that for any type `M` with a monoid structure, any type `α` with a topological space structure and a multiplication action of `M` on `α`, if the action is minimal, then for any element `x` of type `α` and any open set `U` that is not empty, there exists an element `c` of type `M` such that the multiplication action of `c` on `x` results in an element that belongs to `U`.
More concisely: For any monoid `M` acting minimally on a topological space `α`, given a non-empty open set `U` in `α`, there exists an element `c` in `M` such that the multiplication action of `c` on any point `x` in `U` results in a point in `U`.
|
IsOpen.exists_vadd_mem
theorem IsOpen.exists_vadd_mem :
∀ (M : Type u_1) {α : Type u_3} [inst : AddMonoid M] [inst_1 : TopologicalSpace α] [inst_2 : AddAction M α]
[inst_3 : AddAction.IsMinimal M α] (x : α) {U : Set α}, IsOpen U → U.Nonempty → ∃ c, c +ᵥ x ∈ U
The theorem `IsOpen.exists_vadd_mem` states that for any type `M`, and a type `α` with an `AddMonoid` structure, a `TopologicalSpace` structure, and an `AddAction.IsMinimal` structure, given any element `x` of type `α` and an open set `U` of type `α` that is non-empty, there exists an element `c` of type `M` such that the 'additive action' of `c` and `x` (represented by `c +ᵥ x`) is an element of `U`. This theorem is a key result relating additive actions to topological structures, particularly relevant in the context of topological vector spaces.
More concisely: For any `M`, `α` with `AddMonoid`, `TopologicalSpace`, and `AddAction.IsMinimal` structures, given a non-empty open set `U` of `α` and an element `x` of `α`, there exists an element `c` in `M` such that `c +ᵥ x` is in `U`.
|