OpenSubgroup.isOpen
theorem OpenSubgroup.isOpen :
∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] (U : OpenSubgroup G), IsOpen ↑U
The theorem `OpenSubgroup.isOpen` states that for any type `G` that has a group structure and a topology, every open subgroup `U` of `G` is open in the ambient topological space on `G`. Here, the term "open subgroup" refers to a subgroup that is also an open set in the given topology.
More concisely: Every open subgroup of a topological group is open in the group's topology.
|
AddSubgroup.isOpen_mono
theorem AddSubgroup.isOpen_mono :
∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : ContinuousAdd G]
{H₁ H₂ : AddSubgroup G}, H₁ ≤ H₂ → IsOpen ↑H₁ → IsOpen ↑H₂
The theorem `AddSubgroup.isOpen_mono` states that for any type `G` that has both an additive group structure and a topology (with the addition operation being continuous) and given two additive subgroups `H₁` and `H₂` of `G`, if `H₁` is a subset of (or equal to) `H₂` and `H₁` is an open set in the topological space, then `H₂` is also an open set. The symbol `↑` is used to denote the coercion from an additive subgroup to the underlying set.
More concisely: If `H₁` is an open additive subgroup of `G` and `H₁ ⊆ H₂`, then `H₂` is an open subgroup of `G`.
|
AddSubgroup.isOpen_of_zero_mem_interior
theorem AddSubgroup.isOpen_of_zero_mem_interior :
∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : ContinuousAdd G] (H : AddSubgroup G),
0 ∈ interior ↑H → IsOpen ↑H
This theorem states that for any given additive subgroup `H` of a type `G`, given that `G` is an AddGroup, a TopologicalSpace, and has continuous addition, if the interior of `H` contains the additive identity `0`, then `H` is an open set in the underlying topological space. In other words, if `0` is in the interior of an additive subgroup of a topological group with continuous addition, then that subgroup is open.
More concisely: In a topological group with continuous addition, an additive subgroup containing the identity as an interior point is an open set.
|
Subgroup.isOpen_of_one_mem_interior
theorem Subgroup.isOpen_of_one_mem_interior :
∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : ContinuousMul G] (H : Subgroup G),
1 ∈ interior ↑H → IsOpen ↑H
This theorem states that for any subgroup `H` of a topological group `G` (where `G` is a group, a topological space, and the multiplication operation is continuous), if the identity element (`1`) of the group belongs to the interior of `H`, then `H` is an open set in the topological space. In topological terms, the "interior" of a set is the largest open subset within that set, and a set is said to be "open" if it matches certain properties in the context of the topological space.
More concisely: If a subgroup of a topological group contains the identity element in its interior, then the subgroup is open.
|
Subgroup.isOpen_of_mem_nhds
theorem Subgroup.isOpen_of_mem_nhds :
∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : ContinuousMul G] (H : Subgroup G) {g : G},
↑H ∈ nhds g → IsOpen ↑H
This theorem states that for any type `G` which has a group structure, a topological space structure, and where the multiplication operation is continuous, if `H` is a subgroup of `G` and `H` belongs to the neighborhood filter of an element `g` in `G`, then `H` is an open set in the topological space `G`. In other words, if a subgroup is in the neighborhood of a group element, then that subgroup is an open set.
More concisely: If `G` is a topological group and `H` is a subgroup of `G` such that `H` is in the neighborhood filter of some element in `G`, then `H` is open in `G`.
|
OpenAddSubgroup.isOpen
theorem OpenAddSubgroup.isOpen :
∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] (U : OpenAddSubgroup G), IsOpen ↑U
The theorem named `OpenAddSubgroup.isOpen` asserts that for any given additively grouped type `G` (which is also topologically structured), every open additive subgroup `U` of `G` is an open set in the ambient topological space on `G`. Here, open set is defined in the topological sense, which means it is a set where around every point in the set, there exists an open ball that is completely contained in the set. This theorem is an important attribute of open additive subgroups in the context of topological groups.
More concisely: Every open additive subgroup of a topologically structured additive group is an open set.
|