mathlib documentation

topology.algebra.open_subgroup

structure open_add_subgroup (G : Type u_1) [add_group G] [topological_space G] :
Type u_1

The type of open subgroups of a topological additive group.

Reinterpret an open_subgroup as a subgroup.

structure open_subgroup (G : Type u_1) [group G] [topological_space G] :
Type u_1

The type of open subgroups of a topological group.

@[instance]

Equations
@[instance]
def open_subgroup.has_mem {G : Type u_1} [group G] [topological_space G] :

Equations
@[instance]

@[simp]
theorem open_subgroup.mem_coe {G : Type u_1} [group G] [topological_space G] {U : open_subgroup G} {g : G} :
g U g U

@[simp]
theorem open_add_subgroup.mem_coe {G : Type u_1} [add_group G] [topological_space G] {U : open_add_subgroup G} {g : G} :
g U g U

@[simp]
theorem open_add_subgroup.mem_coe_opens {G : Type u_1} [add_group G] [topological_space G] {U : open_add_subgroup G} {g : G} :
g U g U

@[simp]
theorem open_subgroup.mem_coe_opens {G : Type u_1} [group G] [topological_space G] {U : open_subgroup G} {g : G} :
g U g U

@[simp]
theorem open_add_subgroup.mem_coe_add_subgroup {G : Type u_1} [add_group G] [topological_space G] {U : open_add_subgroup G} {g : G} :
g U g U

@[simp]
theorem open_subgroup.mem_coe_subgroup {G : Type u_1} [group G] [topological_space G] {U : open_subgroup G} {g : G} :
g U g U

@[ext]
theorem open_subgroup.ext {G : Type u_1} [group G] [topological_space G] {U V : open_subgroup G} :
(∀ (x : G), x U x V)U = V

theorem open_add_subgroup.ext {G : Type u_1} [add_group G] [topological_space G] {U V : open_add_subgroup G} :
(∀ (x : G), x U x V)U = V

theorem open_subgroup.ext_iff {G : Type u_1} [group G] [topological_space G] {U V : open_subgroup G} :
U = V ∀ (x : G), x U x V

theorem open_add_subgroup.ext_iff {G : Type u_1} [add_group G] [topological_space G] {U V : open_add_subgroup G} :
U = V ∀ (x : G), x U x V

theorem open_subgroup.is_open {G : Type u_1} [group G] [topological_space G] (U : open_subgroup G) :

theorem open_subgroup.one_mem {G : Type u_1} [group G] [topological_space G] (U : open_subgroup G) :
1 U

theorem open_add_subgroup.zero_mem {G : Type u_1} [add_group G] [topological_space G] (U : open_add_subgroup G) :
0 U

theorem open_subgroup.inv_mem {G : Type u_1} [group G] [topological_space G] (U : open_subgroup G) {g : G} :
g Ug⁻¹ U

theorem open_add_subgroup.neg_mem {G : Type u_1} [add_group G] [topological_space G] (U : open_add_subgroup G) {g : G} :
g U-g U

theorem open_add_subgroup.add_mem {G : Type u_1} [add_group G] [topological_space G] (U : open_add_subgroup G) {g₁ g₂ : G} :
g₁ Ug₂ Ug₁ + g₂ U

theorem open_subgroup.mul_mem {G : Type u_1} [group G] [topological_space G] (U : open_subgroup G) {g₁ g₂ : G} :
g₁ Ug₂ Ug₁ * g₂ U

theorem open_subgroup.mem_nhds_one {G : Type u_1} [group G] [topological_space G] (U : open_subgroup G) :

@[instance]

Equations
def open_subgroup.prod {G : Type u_1} [group G] [topological_space G] {H : Type u_2} [group H] [topological_space H] :

The product of two open subgroups as an open subgroup of the product group.

Equations

The product of two open subgroups as an open subgroup of the product group.

@[simp]
theorem open_subgroup.coe_inf {G : Type u_1} [group G] [topological_space G] {U V : open_subgroup G} :
(U V) = U V

@[simp]
theorem open_add_subgroup.coe_inf {G : Type u_1} [add_group G] [topological_space G] {U V : open_add_subgroup G} :
(U V) = U V

@[simp]
theorem open_subgroup.coe_subset {G : Type u_1} [group G] [topological_space G] {U V : open_subgroup G} :
U V U V

@[simp]
theorem open_add_subgroup.coe_subset {G : Type u_1} [add_group G] [topological_space G] {U V : open_add_subgroup G} :
U V U V

@[simp]

@[simp]
theorem open_subgroup.coe_subgroup_le {G : Type u_1} [group G] [topological_space G] {U V : open_subgroup G} :
U V U V

theorem subgroup.is_open_of_mem_nhds {G : Type u_1} [group G] [topological_space G] [has_continuous_mul G] (H : subgroup G) {g : G} :

theorem subgroup.is_open_mono {G : Type u_1} [group G] [topological_space G] [has_continuous_mul G] {H₁ H₂ : subgroup G} :
H₁ H₂is_open H₁is_open H₂

theorem add_subgroup.is_open_mono {G : Type u_1} [add_group G] [topological_space G] [has_continuous_add G] {H₁ H₂ : add_subgroup G} :
H₁ H₂is_open H₁is_open H₂

theorem submodule.is_open_mono {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [topological_space M] [topological_add_group M] [module R M] {U P : submodule R M} :
U Pis_open Uis_open P

theorem ideal.is_open_of_open_subideal {R : Type u_1} [comm_ring R] [topological_space R] [topological_ring R] {U I : ideal R} :
U Iis_open Uis_open I