# mathlib3documentation

topology.algebra.group.basic

# Topological groups #

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

This file defines the following typeclasses:

• `topological_group`, `topological_add_group`: multiplicative and additive topological groups, i.e., groups with continuous `(*)` and `(⁻¹)` / `(+)` and `(-)`;

• `has_continuous_sub G` means that `G` has a continuous subtraction operation.

There is an instance deducing `has_continuous_sub` from `topological_group` but we use a separate typeclass because, e.g., `ℕ` and `ℝ≥0` have continuous subtraction but are not additive groups.

We also define `homeomorph` versions of several `equiv`s: `homeomorph.mul_left`, `homeomorph.mul_right`, `homeomorph.inv`, and prove a few facts about neighbourhood filters in groups.

## Tags #

topological space, group, topological group

### Groups with continuous multiplication #

In this section we prove a few statements about groups with continuous `(*)`.

@[protected]
def homeomorph.add_left {G : Type w} [add_group G] (a : G) :
G ≃ₜ G

Addition from the left in a topological additive group as a homeomorphism.

Equations
@[protected]
def homeomorph.mul_left {G : Type w} [group G] (a : G) :
G ≃ₜ G

Multiplication from the left in a topological group as a homeomorphism.

Equations
@[simp]
theorem homeomorph.coe_add_left {G : Type w} [add_group G] (a : G) :
@[simp]
theorem homeomorph.coe_mul_left {G : Type w} [group G] (a : G) :
theorem homeomorph.add_left_symm {G : Type w} [add_group G] (a : G) :
theorem homeomorph.mul_left_symm {G : Type w} [group G] (a : G) :
theorem is_open_map_add_left {G : Type w} [add_group G] (a : G) :
is_open_map (λ (x : G), a + x)
theorem is_open_map_mul_left {G : Type w} [group G] (a : G) :
is_open_map (λ (x : G), a * x)
theorem is_open.left_add_coset {G : Type w} [add_group G] {U : set G} (h : is_open U) (x : G) :
theorem is_open.left_coset {G : Type w} [group G] {U : set G} (h : is_open U) (x : G) :
theorem is_closed_map_mul_left {G : Type w} [group G] (a : G) :
is_closed_map (λ (x : G), a * x)
theorem is_closed_map_add_left {G : Type w} [add_group G] (a : G) :
is_closed_map (λ (x : G), a + x)
theorem is_closed.left_add_coset {G : Type w} [add_group G] {U : set G} (h : is_closed U) (x : G) :
theorem is_closed.left_coset {G : Type w} [group G] {U : set G} (h : is_closed U) (x : G) :
@[protected]
def homeomorph.add_right {G : Type w} [add_group G] (a : G) :
G ≃ₜ G

Addition from the right in a topological additive group as a homeomorphism.

Equations
@[protected]
def homeomorph.mul_right {G : Type w} [group G] (a : G) :
G ≃ₜ G

Multiplication from the right in a topological group as a homeomorphism.

Equations
@[simp]
theorem homeomorph.coe_mul_right {G : Type w} [group G] (a : G) :
= λ (g : G), g * a
@[simp]
theorem homeomorph.coe_add_right {G : Type w} [add_group G] (a : G) :
= λ (g : G), g + a
theorem homeomorph.mul_right_symm {G : Type w} [group G] (a : G) :
theorem homeomorph.add_right_symm {G : Type w} [add_group G] (a : G) :
theorem is_open_map_mul_right {G : Type w} [group G] (a : G) :
is_open_map (λ (x : G), x * a)
theorem is_open_map_add_right {G : Type w} [add_group G] (a : G) :
is_open_map (λ (x : G), x + a)
theorem is_open.right_coset {G : Type w} [group G] {U : set G} (h : is_open U) (x : G) :
theorem is_open.right_add_coset {G : Type w} [add_group G] {U : set G} (h : is_open U) (x : G) :
theorem is_closed_map_mul_right {G : Type w} [group G] (a : G) :
is_closed_map (λ (x : G), x * a)
theorem is_closed_map_add_right {G : Type w} [add_group G] (a : G) :
is_closed_map (λ (x : G), x + a)
theorem is_closed.right_coset {G : Type w} [group G] {U : set G} (h : is_closed U) (x : G) :
theorem is_closed.right_add_coset {G : Type w} [add_group G] {U : set G} (h : is_closed U) (x : G) :

### `has_continuous_inv` and `has_continuous_neg`#

@[class]
structure has_continuous_neg (G : Type u) [has_neg G] :
Prop

Basic hypothesis to talk about a topological additive group. A topological additive group over `M`, for example, is obtained by requiring the instances `add_group M` and `has_continuous_add M` and `has_continuous_neg M`.

Instances of this typeclass
@[class]
structure has_continuous_inv (G : Type u) [has_inv G] :
Prop

Basic hypothesis to talk about a topological group. A topological group over `M`, for example, is obtained by requiring the instances `group M` and `has_continuous_mul M` and `has_continuous_inv M`.

Instances of this typeclass
theorem continuous_on_inv {G : Type w} [has_inv G] {s : set G} :
theorem continuous_on_neg {G : Type w} [has_neg G] {s : set G} :
theorem continuous_within_at_inv {G : Type w} [has_inv G] {s : set G} {x : G} :
theorem continuous_within_at_neg {G : Type w} [has_neg G] {s : set G} {x : G} :
theorem continuous_at_neg {G : Type w} [has_neg G] {x : G} :
theorem continuous_at_inv {G : Type w} [has_inv G] {x : G} :
theorem tendsto_inv {G : Type w} [has_inv G] (a : G) :
theorem tendsto_neg {G : Type w} [has_neg G] (a : G) :
(nhds (-a))
theorem filter.tendsto.inv {α : Type u} {G : Type w} [has_inv G] {f : α G} {l : filter α} {y : G} (h : (nhds y)) :
filter.tendsto (λ (x : α), (f x)⁻¹) l (nhds y⁻¹)

If a function converges to a value in a multiplicative topological group, then its inverse converges to the inverse of this value. For the version in normed fields assuming additionally that the limit is nonzero, use `tendsto.inv'`.

theorem filter.tendsto.neg {α : Type u} {G : Type w} [has_neg G] {f : α G} {l : filter α} {y : G} (h : (nhds y)) :
filter.tendsto (λ (x : α), -f x) l (nhds (-y))

If a function converges to a value in an additive topological group, then its negation converges to the negation of this value.

@[continuity]
theorem continuous.inv {α : Type u} {G : Type w} [has_inv G] {f : α G} (hf : continuous f) :
continuous (λ (x : α), (f x)⁻¹)
@[continuity]
theorem continuous.neg {α : Type u} {G : Type w} [has_neg G] {f : α G} (hf : continuous f) :
continuous (λ (x : α), -f x)
theorem continuous_at.neg {α : Type u} {G : Type w} [has_neg G] {f : α G} {x : α} (hf : x) :
continuous_at (λ (x : α), -f x) x
theorem continuous_at.inv {α : Type u} {G : Type w} [has_inv G] {f : α G} {x : α} (hf : x) :
continuous_at (λ (x : α), (f x)⁻¹) x
theorem continuous_on.inv {α : Type u} {G : Type w} [has_inv G] {f : α G} {s : set α} (hf : s) :
continuous_on (λ (x : α), (f x)⁻¹) s
theorem continuous_on.neg {α : Type u} {G : Type w} [has_neg G] {f : α G} {s : set α} (hf : s) :
continuous_on (λ (x : α), -f x) s
theorem continuous_within_at.inv {α : Type u} {G : Type w} [has_inv G] {f : α G} {s : set α} {x : α} (hf : x) :
continuous_within_at (λ (x : α), (f x)⁻¹) s x
theorem continuous_within_at.neg {α : Type u} {G : Type w} [has_neg G] {f : α G} {s : set α} {x : α} (hf : x) :
continuous_within_at (λ (x : α), -f x) s x
@[protected, instance]
def prod.has_continuous_neg {G : Type w} {H : Type x} [has_neg G] [has_neg H]  :
@[protected, instance]
def prod.has_continuous_inv {G : Type w} {H : Type x} [has_inv G] [has_inv H]  :
@[protected, instance]
def pi.has_continuous_inv {ι : Type u_1} {C : ι Type u_2} [Π (i : ι), topological_space (C i)] [Π (i : ι), has_inv (C i)] [ (i : ι), has_continuous_inv (C i)] :
has_continuous_inv (Π (i : ι), C i)
@[protected, instance]
def pi.has_continuous_neg {ι : Type u_1} {C : ι Type u_2} [Π (i : ι), topological_space (C i)] [Π (i : ι), has_neg (C i)] [ (i : ι), has_continuous_neg (C i)] :
has_continuous_neg (Π (i : ι), C i)
@[protected, instance]
def pi.has_continuous_neg' {G : Type w} [has_neg G] {ι : Type u_1} :

A version of `pi.has_continuous_neg` for non-dependent functions. It is needed because sometimes Lean fails to use `pi.has_continuous_neg` for non-dependent functions.

@[protected, instance]
def pi.has_continuous_inv' {G : Type w} [has_inv G] {ι : Type u_1} :

A version of `pi.has_continuous_inv` for non-dependent functions. It is needed because sometimes Lean fails to use `pi.has_continuous_inv` for non-dependent functions.

@[protected, instance]
@[protected, instance]
theorem is_closed_set_of_map_neg (G₁ : Type u_2) (G₂ : Type u_3) [t2_space G₂] [has_neg G₁] [has_neg G₂]  :
is_closed {f : G₁ G₂ | (x : G₁), f (-x) = -f x}
theorem is_closed_set_of_map_inv (G₁ : Type u_2) (G₂ : Type u_3) [t2_space G₂] [has_inv G₁] [has_inv G₂]  :
is_closed {f : G₁ G₂ | (x : G₁), f x⁻¹ = (f x)⁻¹}
@[protected, instance]
@[protected, instance]
theorem is_compact.neg {G : Type w} {s : set G} (hs : is_compact s) :
theorem is_compact.inv {G : Type w} {s : set G} (hs : is_compact s) :
@[protected]
def homeomorph.neg (G : Type u_1)  :
G ≃ₜ G

Negation in a topological group as a homeomorphism.

Equations
@[protected]
def homeomorph.inv (G : Type u_1)  :
G ≃ₜ G

Inversion in a topological group as a homeomorphism.

Equations
theorem is_open_map_neg (G : Type w)  :
theorem is_open_map_inv (G : Type w)  :
theorem is_closed_map_inv (G : Type w)  :
theorem is_closed_map_neg (G : Type w)  :
theorem is_open.inv {G : Type w} {s : set G} (hs : is_open s) :
theorem is_open.neg {G : Type w} {s : set G} (hs : is_open s) :
theorem is_closed.neg {G : Type w} {s : set G} (hs : is_closed s) :
theorem is_closed.inv {G : Type w} {s : set G} (hs : is_closed s) :
theorem neg_closure {G : Type w} (s : set G) :
theorem inv_closure {G : Type w} (s : set G) :
theorem has_continuous_neg_Inf {G : Type w} [has_neg G] {ts : set } (h : (t : , t ts ) :
theorem has_continuous_inv_Inf {G : Type w} [has_inv G] {ts : set } (h : (t : , t ts ) :
theorem has_continuous_inv_infi {G : Type w} {ι' : Sort u_1} [has_inv G] {ts' : ι' } (h' : (i : ι'), ) :
theorem has_continuous_neg_infi {G : Type w} {ι' : Sort u_1} [has_neg G] {ts' : ι' } (h' : (i : ι'), ) :
theorem has_continuous_inv_inf {G : Type w} [has_inv G] {t₁ t₂ : topological_space G} (h₁ : has_continuous_inv G) (h₂ : has_continuous_inv G) :
theorem has_continuous_neg_inf {G : Type w} [has_neg G] {t₁ t₂ : topological_space G} (h₁ : has_continuous_neg G) (h₂ : has_continuous_neg G) :
theorem inducing.has_continuous_neg {G : Type u_1} {H : Type u_2} [has_neg G] [has_neg H] {f : G H} (hf : inducing f) (hf_inv : (x : G), f (-x) = -f x) :
theorem inducing.has_continuous_inv {G : Type u_1} {H : Type u_2} [has_inv G] [has_inv H] {f : G H} (hf : inducing f) (hf_inv : (x : G), f x⁻¹ = (f x)⁻¹) :

### Topological groups #

A topological group is a group in which the multiplication and inversion operations are continuous. Topological additive groups are defined in the same way. Equivalently, we can require that the division operation `λ x y, x * y⁻¹` (resp., subtraction) is continuous.

@[class]
Prop
• to_has_continuous_neg :

A topological (additive) group is a group in which the addition and negation operations are continuous.

Instances of this typeclass
@[class]
structure topological_group (G : Type u_1) [group G] :
Prop
• to_has_continuous_mul :
• to_has_continuous_inv :

A topological group is a group in which the multiplication and inversion operations are continuous.

When you declare an instance that does not already have a `uniform_space` instance, you should also provide an instance of `uniform_space` and `uniform_group` using `topological_group.to_uniform_space` and `topological_comm_group_is_uniform`.

Instances of this typeclass
@[protected, instance]
theorem topological_group.continuous_conj_prod {G : Type w} [has_inv G] [has_mul G]  :
continuous (λ (g : G × G), g.fst * g.snd * (g.fst)⁻¹)

Conjugation is jointly continuous on `G × G` when both `mul` and `inv` are continuous.

continuous (λ (g : G × G), g.fst + g.snd + -g.fst)

Conjugation is jointly continuous on `G × G` when both `mul` and `inv` are continuous.

theorem topological_add_group.continuous_conj {G : Type w} [has_neg G] [has_add G] (g : G) :
continuous (λ (h : G), g + h + -g)

Conjugation by a fixed element is continuous when `add` is continuous.

theorem topological_group.continuous_conj {G : Type w} [has_inv G] [has_mul G] (g : G) :
continuous (λ (h : G), g * h * g⁻¹)

Conjugation by a fixed element is continuous when `mul` is continuous.

theorem topological_add_group.continuous_conj' {G : Type w} [has_neg G] [has_add G] (h : G) :
continuous (λ (g : G), g + h + -g)

Conjugation acting on fixed element of the additive group is continuous when both `add` and `neg` are continuous.

theorem topological_group.continuous_conj' {G : Type w} [has_inv G] [has_mul G] (h : G) :
continuous (λ (g : G), g * h * g⁻¹)

Conjugation acting on fixed element of the group is continuous when both `mul` and `inv` are continuous.

@[continuity]
theorem continuous_zpow {G : Type w} [group G] (z : ) :
continuous (λ (a : G), a ^ z)
@[continuity]
theorem continuous_zsmul {G : Type w} [add_group G] (z : ) :
continuous (λ (a : G), z a)
@[protected, instance]
@[protected, instance]
@[continuity]
theorem continuous.zsmul {α : Type u} {G : Type w} [add_group G] {f : α G} (h : continuous f) (z : ) :
continuous (λ (b : α), z f b)
@[continuity]
theorem continuous.zpow {α : Type u} {G : Type w} [group G] {f : α G} (h : continuous f) (z : ) :
continuous (λ (b : α), f b ^ z)
theorem continuous_on_zpow {G : Type w} [group G] {s : set G} (z : ) :
continuous_on (λ (x : G), x ^ z) s
theorem continuous_on_zsmul {G : Type w} [add_group G] {s : set G} (z : ) :
continuous_on (λ (x : G), z x) s
theorem continuous_at_zsmul {G : Type w} [add_group G] (x : G) (z : ) :
continuous_at (λ (x : G), z x) x
theorem continuous_at_zpow {G : Type w} [group G] (x : G) (z : ) :
continuous_at (λ (x : G), x ^ z) x
theorem filter.tendsto.zpow {G : Type w} [group G] {α : Type u_1} {l : filter α} {f : α G} {x : G} (hf : (nhds x)) (z : ) :
filter.tendsto (λ (x : α), f x ^ z) l (nhds (x ^ z))
theorem filter.tendsto.zsmul {G : Type w} [add_group G] {α : Type u_1} {l : filter α} {f : α G} {x : G} (hf : (nhds x)) (z : ) :
filter.tendsto (λ (x : α), z f x) l (nhds (z x))
theorem continuous_within_at.zpow {α : Type u} {G : Type w} [group G] {f : α G} {x : α} {s : set α} (hf : x) (z : ) :
continuous_within_at (λ (x : α), f x ^ z) s x
theorem continuous_within_at.zsmul {α : Type u} {G : Type w} [add_group G] {f : α G} {x : α} {s : set α} (hf : x) (z : ) :
continuous_within_at (λ (x : α), z f x) s x
theorem continuous_at.zsmul {α : Type u} {G : Type w} [add_group G] {f : α G} {x : α} (hf : x) (z : ) :
continuous_at (λ (x : α), z f x) x
theorem continuous_at.zpow {α : Type u} {G : Type w} [group G] {f : α G} {x : α} (hf : x) (z : ) :
continuous_at (λ (x : α), f x ^ z) x
theorem continuous_on.zsmul {α : Type u} {G : Type w} [add_group G] {f : α G} {s : set α} (hf : s) (z : ) :
continuous_on (λ (x : α), z f x) s
theorem continuous_on.zpow {α : Type u} {G : Type w} [group G] {f : α G} {s : set α} (hf : s) (z : ) :
continuous_on (λ (x : α), f x ^ z) s
theorem tendsto_inv_nhds_within_Ioi {H : Type x} {a : H} :
theorem tendsto_neg_nhds_within_Ioi {H : Type x} {a : H} :
(nhds_within (-a) (set.Iio (-a)))
theorem tendsto_inv_nhds_within_Iio {H : Type x} {a : H} :
theorem tendsto_neg_nhds_within_Iio {H : Type x} {a : H} :
(nhds_within (-a) (set.Ioi (-a)))
theorem tendsto_inv_nhds_within_Ioi_inv {H : Type x} {a : H} :
(set.Iio a))
theorem tendsto_neg_nhds_within_Ioi_neg {H : Type x} {a : H} :
(nhds_within (-a) (set.Ioi (-a))) (set.Iio a))
theorem tendsto_inv_nhds_within_Iio_inv {H : Type x} {a : H} :
(set.Ioi a))
theorem tendsto_neg_nhds_within_Iio_neg {H : Type x} {a : H} :
(nhds_within (-a) (set.Iio (-a))) (set.Ioi a))
theorem tendsto_inv_nhds_within_Ici {H : Type x} {a : H} :
theorem tendsto_neg_nhds_within_Ici {H : Type x} {a : H} :
(nhds_within (-a) (set.Iic (-a)))
theorem tendsto_inv_nhds_within_Iic {H : Type x} {a : H} :
theorem tendsto_neg_nhds_within_Iic {H : Type x} {a : H} :
(nhds_within (-a) (set.Ici (-a)))
theorem tendsto_neg_nhds_within_Ici_neg {H : Type x} {a : H} :
(nhds_within (-a) (set.Ici (-a))) (set.Iic a))
theorem tendsto_inv_nhds_within_Ici_inv {H : Type x} {a : H} :
(set.Iic a))
theorem tendsto_neg_nhds_within_Iic_neg {H : Type x} {a : H} :
(nhds_within (-a) (set.Iic (-a))) (set.Ici a))
theorem tendsto_inv_nhds_within_Iic_inv {H : Type x} {a : H} :
(set.Ici a))
@[protected, instance]
@[protected, instance]
def prod.topological_group {G : Type w} {H : Type x} [group G] [group H]  :
@[protected, instance]
def pi.topological_add_group {β : Type v} {C : β Type u_1} [Π (b : β), topological_space (C b)] [Π (b : β), add_group (C b)] [ (b : β), ] :
topological_add_group (Π (b : β), C b)
@[protected, instance]
def pi.topological_group {β : Type v} {C : β Type u_1} [Π (b : β), topological_space (C b)] [Π (b : β), group (C b)] [ (b : β), topological_group (C b)] :
topological_group (Π (b : β), C b)
@[protected, instance]
@[protected, instance]
@[protected, instance]

If addition is continuous in `α`, then it also is in `αᵃᵒᵖ`.

@[protected, instance]
def mul_opposite.topological_group {α : Type u} [group α]  :

If multiplication is continuous in `α`, then it also is in `αᵐᵒᵖ`.

theorem nhds_one_symm (G : Type w) [group G]  :
= nhds 1
theorem nhds_zero_symm (G : Type w) [add_group G]  :
= nhds 0
theorem nhds_one_symm' (G : Type w) [group G]  :
= nhds 1
theorem nhds_zero_symm' (G : Type w) [add_group G]  :
= nhds 0
theorem neg_mem_nhds_zero (G : Type w) [add_group G] {S : set G} (hS : S nhds 0) :
theorem inv_mem_nhds_one (G : Type w) [group G] {S : set G} (hS : S nhds 1) :
@[protected]
def homeomorph.shear_mul_right (G : Type w) [group G]  :
G × G ≃ₜ G × G

The map `(x, y) ↦ (x, xy)` as a homeomorphism. This is a shear mapping.

Equations
@[protected]
G × G ≃ₜ G × G

The map `(x, y) ↦ (x, x + y)` as a homeomorphism. This is a shear mapping.

Equations
@[simp]
theorem homeomorph.shear_mul_right_coe (G : Type w) [group G]  :
= λ (z : G × G), (z.fst, z.fst * z.snd)
@[simp]
= λ (z : G × G), (z.fst, z.fst + z.snd)
@[simp]
= λ (z : G × G), (z.fst, -z.fst + z.snd)
@[simp]
theorem homeomorph.shear_mul_right_symm_coe (G : Type w) [group G]  :
= λ (z : G × G), (z.fst, (z.fst)⁻¹ * z.snd)
@[protected]
theorem inducing.topological_group {G : Type w} {H : Type x} [group G] {F : Type u_1} [group H] [ G] (f : F) (hf : inducing f) :
@[protected]
theorem inducing.topological_add_group {G : Type w} {H : Type x} [add_group G] {F : Type u_1} [add_group H] [ G] (f : F) (hf : inducing f) :
@[protected]
theorem topological_group_induced {G : Type w} {H : Type x} [group G] {F : Type u_1} [group H] [ G] (f : F) :
@[protected]
theorem topological_add_group_induced {G : Type w} {H : Type x} [add_group G] {F : Type u_1} [add_group H] [ G] (f : F) :
@[protected, instance]
@[protected, instance]
def subgroup.topological_group {G : Type w} [group G] (S : subgroup G) :
def subgroup.topological_closure {G : Type w} [group G] (s : subgroup G) :

The (topological-space) closure of a subgroup of a space `M` with `has_continuous_mul` is itself a subgroup.

Equations

The (topological-space) closure of an additive subgroup of a space `M` with `has_continuous_add` is itself an additive subgroup.

Equations
@[simp]
theorem subgroup.topological_closure_coe {G : Type w} [group G] {s : subgroup G} :
@[simp]
theorem subgroup.le_topological_closure {G : Type w} [group G] (s : subgroup G) :
theorem add_subgroup.topological_closure_minimal {G : Type w} [add_group G] (s : add_subgroup G) {t : add_subgroup G} (h : s t) (ht : is_closed t) :
theorem subgroup.topological_closure_minimal {G : Type w} [group G] (s : subgroup G) {t : subgroup G} (h : s t) (ht : is_closed t) :
theorem dense_range.topological_closure_map_subgroup {G : Type w} {H : Type x} [group G] [group H] {f : G →* H} (hf : continuous f) (hf' : dense_range f) {s : subgroup G} (hs : s.topological_closure = ) :

The topological closure of a normal additive subgroup is normal.

theorem subgroup.is_normal_topological_closure {G : Type u_1} [group G] (N : subgroup G) [N.normal] :

The topological closure of a normal subgroup is normal.

theorem mul_mem_connected_component_one {G : Type u_1} {g h : G} (hg : g ) (hh : h ) :
g * h
theorem add_mem_connected_component_zero {G : Type u_1} {g h : G} (hg : g ) (hh : h ) :
g + h
theorem inv_mem_connected_component_one {G : Type u_1} [group G] {g : G} (hg : g ) :
theorem neg_mem_connected_component_zero {G : Type u_1} [add_group G] {g : G} (hg : g ) :

The connected component of 1 is a subgroup of `G`.

Equations

The connected component of 0 is a subgroup of `G`.

Equations
def subgroup.comm_group_topological_closure {G : Type w} [group G] [t2_space G] (s : subgroup G) (hs : (x y : s), x * y = y * x) :

If a subgroup of a topological group is commutative, then so is its topological closure.

Equations
def add_subgroup.add_comm_group_topological_closure {G : Type w} [add_group G] [t2_space G] (s : add_subgroup G) (hs : (x y : s), x + y = y + x) :

If a subgroup of an additive topological group is commutative, then so is its topological closure.

Equations
theorem exists_nhds_half_neg {G : Type w} [add_group G] {s : set G} (hs : s nhds 0) :
(V : set G) (H : V nhds 0), (v : G), v V (w : G), w V v - w s
theorem exists_nhds_split_inv {G : Type w} [group G] {s : set G} (hs : s nhds 1) :
(V : set G) (H : V nhds 1), (v : G), v V (w : G), w V v / w s
theorem nhds_translation_add_neg {G : Type w} [add_group G] (x : G) :
filter.comap (λ (y : G), y + -x) (nhds 0) = nhds x
theorem nhds_translation_mul_inv {G : Type w} [group G] (x : G) :
filter.comap (λ (y : G), y * x⁻¹) (nhds 1) = nhds x
@[simp]
theorem map_add_left_nhds {G : Type w} [add_group G] (x y : G) :
(nhds y) = nhds (x + y)
@[simp]
theorem map_mul_left_nhds {G : Type w} [group G] (x y : G) :
(nhds y) = nhds (x * y)
theorem map_add_left_nhds_zero {G : Type w} [add_group G] (x : G) :
(nhds 0) = nhds x
theorem map_mul_left_nhds_one {G : Type w} [group G] (x : G) :
(nhds 1) = nhds x
@[simp]
theorem map_add_right_nhds {G : Type w} [add_group G] (x y : G) :
filter.map (λ (z : G), z + x) (nhds y) = nhds (y + x)
@[simp]
theorem map_mul_right_nhds {G : Type w} [group G] (x y : G) :
filter.map (λ (z : G), z * x) (nhds y) = nhds (y * x)
theorem map_mul_right_nhds_one {G : Type w} [group G] (x : G) :
filter.map (λ (y : G), y * x) (nhds 1) = nhds x
theorem map_add_right_nhds_zero {G : Type w} [add_group G] (x : G) :
filter.map (λ (y : G), y + x) (nhds 0) = nhds x
theorem filter.has_basis.nhds_of_zero {G : Type w} [add_group G] {ι : Sort u_1} {p : ι Prop} {s : ι set G} (hb : (nhds 0).has_basis p s) (x : G) :
(nhds x).has_basis p (λ (i : ι), {y : G | y - x s i})
theorem filter.has_basis.nhds_of_one {G : Type w} [group G] {ι : Sort u_1} {p : ι Prop} {s : ι set G} (hb : (nhds 1).has_basis p s) (x : G) :
(nhds x).has_basis p (λ (i : ι), {y : G | y / x s i})
theorem mem_closure_iff_nhds_zero {G : Type w} [add_group G] {x : G} {s : set G} :
x (U : set G), U nhds 0 ( (y : G) (H : y s), y - x U)
theorem mem_closure_iff_nhds_one {G : Type w} [group G] {x : G} {s : set G} :
x (U : set G), U nhds 1 ( (y : G) (H : y s), y / x U)
theorem continuous_of_continuous_at_one {G : Type w} [group G] {M : Type u_1} {hom : Type u_2} [ G M] (f : hom) (hf : 1) :

A monoid homomorphism (a bundled morphism of a type that implements `monoid_hom_class`) from a topological group to a topological monoid is continuous provided that it is continuous at one. See also `uniform_continuous_of_continuous_at_one`.

theorem continuous_of_continuous_at_zero {G : Type w} [add_group G] {M : Type u_1} {hom : Type u_2} [ G M] (f : hom) (hf : 0) :

An additive monoid homomorphism (a bundled morphism of a type that implements `add_monoid_hom_class`) from an additive topological group to an additive topological monoid is continuous provided that it is continuous at zero. See also `uniform_continuous_of_continuous_at_zero`.

theorem topological_group.ext {G : Type u_1} [group G] {t t' : topological_space G} (tg : topological_group G) (tg' : topological_group G) (h : nhds 1 = nhds 1) :
t = t'
theorem topological_add_group.ext {G : Type u_1} [add_group G] {t t' : topological_space G} (tg : topological_add_group G) (tg' : topological_add_group G) (h : nhds 0 = nhds 0) :
t = t'
theorem topological_group.ext_iff {G : Type u_1} [group G] {t t' : topological_space G} (tg : topological_group G) (tg' : topological_group G) :
t = t' nhds 1 = nhds 1
theorem has_continuous_inv.of_nhds_one {G : Type u_1} [group G] (hinv : filter.tendsto (λ (x : G), x⁻¹) (nhds 1) (nhds 1)) (hleft : (x₀ : G), nhds x₀ = filter.map (λ (x : G), x₀ * x) (nhds 1)) (hconj : (x₀ : G), filter.tendsto (λ (x : G), x₀ * x * x₀⁻¹) (nhds 1) (nhds 1)) :
theorem has_continuous_neg.of_nhds_zero {G : Type u_1} [add_group G] (hinv : filter.tendsto (λ (x : G), -x) (nhds 0) (nhds 0)) (hleft : (x₀ : G), nhds x₀ = filter.map (λ (x : G), x₀ + x) (nhds 0)) (hconj : (x₀ : G), filter.tendsto (λ (x : G), x₀ + x + -x₀) (nhds 0) (nhds 0)) :
theorem topological_group.of_nhds_one' {G : Type u} [group G] (hmul : ((nhds 1).prod (nhds 1)) (nhds 1)) (hinv : filter.tendsto (λ (x : G), x⁻¹) (nhds 1) (nhds 1)) (hleft : (x₀ : G), nhds x₀ = filter.map (λ (x : G), x₀ * x) (nhds 1)) (hright : (x₀ : G), nhds x₀ = filter.map (λ (x : G), x * x₀) (nhds 1)) :
theorem topological_add_group.of_nhds_zero' {G : Type u} [add_group G] (hmul : ((nhds 0).prod (nhds 0)) (nhds 0)) (hinv : filter.tendsto (λ (x : G), -x) (nhds 0) (nhds 0)) (hleft : (x₀ : G), nhds x₀ = filter.map (λ (x : G), x₀ + x) (nhds 0)) (hright : (x₀ : G), nhds x₀ = filter.map (λ (x : G), x + x₀) (nhds 0)) :
theorem topological_add_group.of_nhds_zero {G : Type u} [add_group G] (hmul : ((nhds 0).prod (nhds 0)) (nhds 0)) (hinv : filter.tendsto (λ (x : G), -x) (nhds 0) (nhds 0)) (hleft : (x₀ : G), nhds x₀ = filter.map (λ (x : G), x₀ + x) (nhds 0)) (hconj : (x₀ : G), filter.tendsto (λ (x : G), x₀ + x + -x₀) (nhds 0) (nhds 0)) :
theorem topological_group.of_nhds_one {G : Type u} [group G] (hmul : ((nhds 1).prod (nhds 1)) (nhds 1)) (hinv : filter.tendsto (λ (x : G), x⁻¹) (nhds 1) (nhds 1)) (hleft : (x₀ : G), nhds x₀ = filter.map (λ (x : G), x₀ * x) (nhds 1)) (hconj : (x₀ : G), filter.tendsto (λ (x : G), x₀ * x * x₀⁻¹) (nhds 1) (nhds 1)) :
theorem topological_add_group.of_comm_of_nhds_zero {G : Type u} (hmul : ((nhds 0).prod (nhds 0)) (nhds 0)) (hinv : filter.tendsto (λ (x : G), -x) (nhds 0) (nhds 0)) (hleft : (x₀ : G), nhds x₀ = filter.map (λ (x : G), x₀ + x) (nhds 0)) :
theorem topological_group.of_comm_of_nhds_one {G : Type u} [comm_group G] (hmul : ((nhds 1).prod (nhds 1)) (nhds 1)) (hinv : filter.tendsto (λ (x : G), x⁻¹) (nhds 1) (nhds 1)) (hleft : (x₀ : G), nhds x₀ = filter.map (λ (x : G), x₀ * x) (nhds 1)) :
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem quotient_group.is_open_map_coe {G : Type w} [group G] (N : subgroup G) :
@[protected, instance]
@[protected, instance]
= (nhds x)

Neighborhoods in the quotient are precisely the map of neighborhoods in the prequotient.

theorem quotient_group.nhds_eq {G : Type w} [group G] (N : subgroup G) (x : G) :
= (nhds x)

Neighborhoods in the quotient are precisely the map of neighborhoods in the prequotient.

(u : set G), u (n : ), u (n + 1) + u (n + 1) u n

Any first countable topological additive group has an antitone neighborhood basis `u : ℕ → set G` for which `u (n + 1) + u (n + 1) ⊆ u n`. The existence of such a neighborhood basis is a key tool for `quotient_add_group.complete_space`

theorem topological_group.exists_antitone_basis_nhds_one (G : Type w) [group G]  :
(u : set G), u (n : ), u (n + 1) * u (n + 1) u n

Any first countable topological group has an antitone neighborhood basis `u : ℕ → set G` for which `(u (n + 1)) ^ 2 ⊆ u n`. The existence of such a neighborhood basis is a key tool for `quotient_group.complete_space`

@[protected, instance]

In a first countable topological additive group `G` with normal additive subgroup `N`, `0 : G ⧸ N` has a countable neighborhood basis.

@[protected, instance]

In a first countable topological group `G` with normal subgroup `N`, `1 : G ⧸ N` has a countable neighborhood basis.

@[class]
structure has_continuous_sub (G : Type u_1) [has_sub G] :
Prop

A typeclass saying that `λ p : G × G, p.1 - p.2` is a continuous function. This property automatically holds for topological additive groups but it also holds, e.g., for `ℝ≥0`.

Instances of this typeclass
@[class]
structure has_continuous_div (G : Type u_1) [has_div G] :
Prop

A typeclass saying that `λ p : G × G, p.1 / p.2` is a continuous function. This property automatically holds for topological groups. Lemmas using this class have primes. The unprimed version is for `group_with_zero`.

Instances of this typeclass
@[protected, instance]
@[protected, instance]
theorem filter.tendsto.div' {α : Type u} {G : Type w} [has_div G] {f g : α G} {l : filter α} {a b : G} (hf : (nhds a)) (hg : (nhds b)) :
filter.tendsto (λ (x : α), f x / g x) l (nhds (a / b))
theorem filter.tendsto.sub {α : Type u} {G : Type w} [has_sub G] {f g : α G} {l : filter α} {a b : G} (hf : (nhds a)) (hg : (nhds b)) :
filter.tendsto (λ (x : α), f x - g x) l (nhds (a - b))
theorem filter.tendsto.const_sub {α : Type u} {G : Type w} [has_sub G] (b : G) {c : G} {f : α G} {l : filter α} (h : (nhds c)) :
filter.tendsto (λ (k : α), b - f k) l (nhds (b - c))
theorem filter.tendsto.const_div' {α : Type u} {G : Type w} [has_div G] (b : G) {c : G} {f : α G} {l : filter α} (h : (nhds c)) :
filter.tendsto (λ (k : α), b / f k) l (nhds (b / c))
theorem filter.tendsto.div_const' {α : Type u} {G : Type w} [has_div G] {c : G} {f : α G} {l : filter α} (h : (nhds c)) (b : G) :
filter.tendsto (λ (k : α), f k / b) l (nhds (c / b))
theorem filter.tendsto.sub_const {α : Type u} {G : Type w} [has_sub G] {c : G} {f : α G} {l : filter α} (h : (nhds c)) (b : G) :
filter.tendsto (λ (k : α), f k - b) l (nhds (c - b))
@[continuity]
theorem continuous.div' {α : Type u} {G : Type w} [has_div G] {f g : α G} (hf : continuous f) (hg : continuous g) :
continuous (λ (x : α), f x / g x)
@[continuity]
theorem continuous.sub {α : Type u} {G : Type w} [has_sub G] {f g : α G} (hf : continuous f) (hg : continuous g) :
continuous (λ (x : α), f x - g x)
theorem continuous_sub_left {G : Type w} [has_sub G] (a : G) :
continuous (λ (b : G), a - b)
theorem continuous_div_left' {G : Type w} [has_div G] (a : G) :
continuous (λ (b : G), a / b)
theorem continuous_sub_right {G : Type w} [has_sub G] (a : G) :
continuous (λ (b : G), b - a)
theorem continuous_div_right' {G : Type w} [has_div G] (a : G) :
continuous (λ (b : G), b / a)
theorem continuous_at.div' {α : Type u} {G : Type w} [has_div G] {f g : α G} {x : α} (hf : x) (hg : x) :
continuous_at (λ (x : α), f x / g x) x
theorem continuous_at.sub {α : Type u} {G : Type w} [has_sub G] {f g : α G} {x : α} (hf : x) (hg : x) :
continuous_at (λ (x : α), f x - g x) x
theorem continuous_within_at.sub {α : Type u} {G : Type w} [has_sub G] {f g : α G} {s : set α} {x : α} (hf : x) (hg : x) :
continuous_within_at (λ (x : α), f x - g x) s x
theorem continuous_within_at.div' {α : Type u} {G : Type w} [has_div G] {f g : α G} {s : set α} {x : α} (hf : x) (hg : x) :
continuous_within_at (λ (x : α), f x / g x) s x
theorem continuous_on.sub {α : Type u} {G : Type w} [has_sub G] {f g : α G} {s : set α} (hf : s) (hg : s) :
continuous_on (λ (x : α), f x - g x) s
theorem continuous_on.div' {α : Type u} {G : Type w} [has_div G] {f g : α G} {s : set α} (hf : s) (hg : s) :
continuous_on (λ (x : α), f x / g x) s
@[simp]
theorem homeomorph.sub_left_symm_apply {G : Type w} [add_group G] (x ᾰ : G) :
.symm) = -+ x
def homeomorph.div_left {G : Type w} [group G] (x : G) :
G ≃ₜ G

A version of `homeomorph.mul_left a b⁻¹` that is defeq to `a / b`.

Equations
def homeomorph.sub_left {G : Type w} [add_group G] (x : G) :
G ≃ₜ G

A version of `homeomorph.add_left a (-b)` that is defeq to `a - b`.

Equations
@[simp]
theorem homeomorph.div_left_symm_apply {G : Type w} [group G] (x ᾰ : G) :
.symm) = ⁻¹ * x
@[simp]
theorem homeomorph.sub_left_apply {G : Type w} [add_group G] (x ᾰ : G) :
= x -
@[simp]
theorem homeomorph.div_left_apply {G : Type w} [group G] (x ᾰ : G) :
= x /
theorem is_open_map_div_left {G : Type w} [group G] (a : G) :
theorem is_open_map_sub_left {G : Type w} [add_group G] (a : G) :
theorem is_closed_map_div_left {G : Type w} [group G] (a : G) :
theorem is_closed_map_sub_left {G : Type w} [add_group G] (a : G) :
@[simp]
theorem homeomorph.sub_right_symm_apply {G : Type w} [add_group G] (x ᾰ : G) :
.symm) = + x
@[simp]
theorem homeomorph.div_right_symm_apply {G : Type w} [group G] (x ᾰ : G) :
.symm) = * x
@[simp]
theorem homeomorph.sub_right_apply {G : Type w} [add_group G] (x ᾰ : G) :
= - x
@[simp]
theorem homeomorph.div_right_apply {G : Type w} [group G] (x ᾰ : G) :
= / x
def homeomorph.div_right {G : Type w} [group G] (x : G) :
G ≃ₜ G

A version of `homeomorph.mul_right a⁻¹ b` that is defeq to `b / a`.

Equations
def homeomorph.sub_right {G : Type w} [add_group G] (x : G) :
G ≃ₜ G

A version of `homeomorph.add_right (-a) b` that is defeq to `b - a`.

Equations
theorem is_open_map_sub_right {G : Type w} [add_group G] (a : G) :
is_open_map (λ (x : G), x - a)
theorem is_open_map_div_right {G : Type w} [group G] (a : G) :
is_open_map (λ (x : G), x / a)
theorem is_closed_map_sub_right {G : Type w} [add_group G] (a : G) :
is_closed_map (λ (x : G), x - a)
theorem is_closed_map_div_right {G : Type w} [group G] (a : G) :
is_closed_map (λ (x : G), x / a)
theorem tendsto_div_nhds_one_iff {G : Type w} [group G] {α : Type u_1} {l : filter α} {x : G} {u : α G} :
filter.tendsto (λ (n : α), u n / x) l (nhds 1) (nhds x)
theorem tendsto_sub_nhds_zero_iff {G : Type w} [add_group G] {α : Type u_1} {l : filter α} {x : G} {u : α G} :
filter.tendsto (λ (n : α), u n - x) l (nhds 0) (nhds x)
theorem nhds_translation_div {G : Type w} [group G] (x : G) :
filter.comap (λ (_x : G), _x / x) (nhds 1) = nhds x
theorem nhds_translation_sub {G : Type w} [add_group G] (x : G) :
filter.comap (λ (_x : G), _x - x) (nhds 0) = nhds x

### Topological operations on pointwise sums and products #

A few results about interior and closure of the pointwise addition/multiplication of sets in groups with continuous addition/multiplication. See also `submonoid.top_closure_mul_self_eq` in `topology.algebra.monoid`.

theorem is_open.vadd_left {α : Type u} {β : Type v} [add_group α] [ β] {s : set α} {t : set β} (ht : is_open t) :
theorem is_open.smul_left {α : Type u} {β : Type v} [group α] [ β] {s : set α} {t : set β} (ht : is_open t) :
is_open (s t)
theorem subset_interior_smul_right {α : Type u} {β : Type v} [group α] [ β] {s : set α} {t : set β} :
theorem subset_interior_vadd_right {α : Type u} {β : Type v} [add_group α] [ β] {s : set α} {t : set β} :
theorem vadd_mem_nhds {α : Type u} {β : Type v} [add_group α] [ β] {t : set β} (a : α) {x : β} (ht : t nhds x) :
a +ᵥ t nhds (a +ᵥ x)
theorem smul_mem_nhds {α : Type u} {β : Type v} [group α] [ β] {t : set β} (a : α) {x : β} (ht : t nhds x) :
a t nhds (a x)
theorem subset_interior_smul {α : Type u} {β : Type v} [group α] [ β] {s : set α} {t : set β}  :
theorem subset_interior_vadd {α : Type u} {β : Type v} [add_group α] [ β] {s : set α} {t : set β}  :
theorem is_open.mul_left {α : Type u} [group α] {s t : set α} :
is_open (s * t)
theorem is_open.add_left {α : Type u} [add_group α] {s t : set α} :
is_open (s + t)
theorem subset_interior_add_right {α : Type u} [add_group α] {s t : set α} :
s + interior (s + t)
theorem subset_interior_mul_right {α : Type u} [group α] {s t : set α} :
s * interior (s * t)
theorem subset_interior_add {α : Type u} [add_group α] {s t : set α} :
interior (s + t)
theorem subset_interior_mul {α : Type u} [group α] {s t : set α} :
interior (s * t)
theorem singleton_mul_mem_nhds {α : Type u} [group α] {s : set α} (a : α) {b : α} (h : s nhds b) :
{a} * s nhds (a * b)
theorem singleton_add_mem_nhds {α : Type u} [add_group α] {s : set α} (a : α) {b : α} (h : s nhds b) :
{a} + s nhds (a + b)
theorem singleton_mul_mem_nhds_of_nhds_one {α : Type u} [group α] {s : set α} (a : α) (h : s nhds 1) :
{a} * s nhds a
theorem singleton_add_mem_nhds_of_nhds_zero {α : Type u} [add_group α] {s : set α} (a : α) (h : s nhds 0) :
{a} + s nhds a
theorem is_open.mul_right {α : Type u} [group α] {s t : set α} (hs : is_open s) :
is_open (s * t)
theorem is_open.add_right {α : Type u} [add_group α] {s t : set α} (hs : is_open s) :
is_open (s + t)
theorem subset_interior_mul_left {α : Type u} [group α] {s t : set α} :
* t interior (s * t)
theorem subset_interior_add_left {α : Type u} [add_group α] {s t : set α} :
+ t interior (s + t)
theorem subset_interior_mul' {α : Type u} [group α] {s t : set α} :
interior (s * t)
theorem subset_interior_add' {α : Type u} [add_group α] {s t : set α} :
interior (s + t)
theorem add_singleton_mem_nhds {α : Type u} [add_group α] {s : set α} (a : α) {b : α} (h : s nhds b) :
s + {a} nhds (b + a)
theorem mul_singleton_mem_nhds {α : Type u} [group α] {s : set α} (a : α) {b : α} (h : s nhds b) :
s * {a} nhds (b * a)
theorem add_singleton_mem_nhds_of_nhds_zero {α : Type u} [add_group α] {s : set α} (a : α) (h : s nhds 0) :
s + {a} nhds a
theorem mul_singleton_mem_nhds_of_nhds_one {α : Type u} [group α] {s : set α} (a : α) (h : s nhds 1) :
s * {a} nhds a
theorem is_open.div_left {α : Type u} [group α] {s t : set α} (ht : is_open t) :
is_open (s / t)
theorem is_open.sub_left {α : Type u} [add_group α] {s t : set α} (ht : is_open t) :
is_open (s - t)
theorem is_open.div_right {α : Type u} [group α] {s t : set α} (hs : is_open s) :
is_open (s / t)
theorem is_open.sub_right {α : Type u} [add_group α] {s t : set α} (hs : is_open s) :
is_open (s - t)
theorem subset_interior_div_left {α : Type u} [group α] {s t : set α} :
/ t interior (s / t)
theorem subset_interior_sub_left {α : Type u} [add_group α] {s t : set α} :
- t interior (s - t)
theorem subset_interior_sub_right {α : Type u} [add_group α] {s t : set α} :
s - interior (s - t)
theorem subset_interior_div_right {α : Type u} [group α] {s t : set α} :
s / interior (s / t)
theorem subset_interior_sub {α : Type u} [add_group α] {s t : set α} :
interior (s - t)
theorem subset_interior_div {α : Type u} [group α] {s t : set α} :
interior (s / t)
theorem is_open.mul_closure {α : Type u} [group α] {s : set α} (hs : is_open s) (t : set α) :
s * = s * t
theorem is_open.add_closure {α : Type u} [add_group α] {s : set α} (hs : is_open s) (t : set α) :
s + = s + t
theorem is_open.closure_add {α : Type u} [add_group α] {t : set α} (ht : is_open t) (s : set α) :
+ t = s + t
theorem is_open.closure_mul {α : Type u} [group α] {t : set α} (ht : is_open t) (s : set α) :
* t = s * t
theorem is_open.sub_closure {α : Type u} [add_group α] {s : set α} (hs : is_open s) (t : set α) :
s - = s - t
theorem is_open.div_closure {α : Type u} [group α] {s : set α} (hs : is_open s) (t : set α) :
s / = s / t
theorem is_open.closure_div {α : Type u} [group α] {t : set α} (ht : is_open t) (s : set α) :
/ t = s / t
theorem is_open.closure_sub {α : Type u} [add_group α] {t : set α} (ht : is_open t) (s : set α) :
- t = s - t
@[class]
structure add_group_with_zero_nhd (G : Type u) :

additive group with a neighbourhood around 0. Only used to construct a topology and uniform space.

This is currently only available for commutative groups, but it can be extended to non-commutative groups too.

Instances for `add_group_with_zero_nhd`
theorem topological_add_group.t1_space (G : Type w) [add_group G] (h : is_closed {0}) :
theorem topological_group.t1_space (G : Type w) [group G] (h : is_closed {1}) :
@[protected, instance]
@[protected, instance]
theorem topological_group.t3_space (G : Type w) [group G] [t0_space G] :
theorem topological_group.t2_space (G : Type w) [group G] [t0_space G] :
@[protected, instance]
@[protected, instance]
def subgroup.t3_quotient_of_is_closed {G : Type w} [group G] (S : subgroup G) [S.normal] [hS : is_closed S] :

A subgroup `S` of a topological group `G` acts on `G` properly discontinuously on the left, if it is discrete in the sense that `S ∩ K` is finite for all compact `K`. (See also `discrete_topology`.)

A subgroup `S` of an additive topological group `G` acts on `G` properly discontinuously on the left, if it is discrete in the sense that `S ∩ K` is finite for all compact `K`. (See also `discrete_topology`.

A subgroup `S` of an additive topological group `G` acts on `G` properly discontinuously on the right, if it is discrete in the sense that `S ∩ K` is finite for all compact `K`. (See also `discrete_topology`.)

If `G` is Hausdorff, this can be combined with `t2_space_of_properly_discontinuous_vadd_of_t2_space` to show that the quotient group `G ⧸ S` is Hausdorff.

A subgroup `S` of a topological group `G` acts on `G` properly discontinuously on the right, if it is discrete in the sense that `S ∩ K` is finite for all compact `K`. (See also `discrete_topology`.)

If `G` is Hausdorff, this can be combined with `t2_space_of_properly_discontinuous_smul_of_t2_space` to show that the quotient group `G ⧸ S` is Hausdorff.

Some results about an open set containing the product of two sets in a topological group.

theorem compact_open_separated_add_right {G : Type w} {K U : set G} (hK : is_compact K) (hU : is_open U) (hKU : K U) :
(V : set G) (H : V nhds 0), K + V U

Given a compact set `K` inside an open set `U`, there is a open neighborhood `V` of `0` such that `K + V ⊆ U`.

theorem compact_open_separated_mul_right {G : Type w} {K U : set G} (hK : is_compact K) (hU : is_open U) (hKU : K U) :
(V : set G) (H : V nhds 1), K * V U

Given a compact set `K` inside an open set `U`, there is a open neighborhood `V` of `1` such that `K * V ⊆ U`.

theorem compact_open_separated_add_left {G : Type w} {K U : set G} (hK : is_compact K) (hU : is_open U) (hKU : K U) :
(V : set G) (H : V nhds 0), V + K U

Given a compact set `K` inside an open set `U`, there is a open neighborhood `V` of `0` such that `V + K ⊆ U`.

theorem compact_open_separated_mul_left {G : Type w} {K U : set G} (hK : is_compact K) (hU : is_open U) (hKU : K U) :
(V : set G) (H : V nhds 1), V * K U

Given a compact set `K` inside an open set `U`, there is a open neighborhood `V` of `1` such that `V * K ⊆ U`.

theorem compact_covered_by_add_left_translates {G : Type w} [add_group G] {K V : set G} (hK : is_compact K) (hV : (interior V).nonempty) :
(t : finset G), K (g : G) (H : g t), (λ (h : G), g + h) ⁻¹' V

A compact set is covered by finitely many left additive translates of a set with non-empty interior.

theorem compact_covered_by_mul_left_translates {G : Type w} [group G] {K V : set G} (hK : is_compact K) (hV : (interior V).nonempty) :
(t : finset G), K (g : G) (H : g t), (λ (h : G), g * h) ⁻¹' V

A compact set is covered by finitely many left multiplicative translates of a set with non-empty interior.

@[protected, instance]

Every locally compact separable topological group is σ-compact. Note: this is not true if we drop the topological group hypothesis.

@[protected, instance]

Every locally compact separable topological group is σ-compact. Note: this is not true if we drop the topological group hypothesis.

theorem exists_disjoint_vadd_of_is_compact {G : Type w} [add_group G] {K L : set G} (hK : is_compact K) (hL : is_compact L) :
(g : G), (g +ᵥ L)

Given two compact sets in a noncompact additive topological group, there is a translate of the second one that is disjoint from the first one.

theorem exists_disjoint_smul_of_is_compact {G : Type w} [group G] {K L : set G} (hK : is_compact K) (hL : is_compact L) :
(g : G), (g L)

Given two compact sets in a noncompact topological group, there is a translate of the second one that is disjoint from the first one.

theorem local_is_compact_is_closed_nhds_of_add_group {G : Type w} [add_group G] {U : set G} (hU : U nhds 0) :
(K : set G), K U 0

In a locally compact additive group, any neighborhood of the identity contains a compact closed neighborhood of the identity, even without separation assumptions on the space.

theorem local_is_compact_is_closed_nhds_of_group {G : Type w} [group G] {U : set G} (hU : U nhds 1) :
(K : set G), K U 1

In a locally compact group, any neighborhood of the identity contains a compact closed neighborhood of the identity, even without separation assumptions on the space.

theorem nhds_mul {G : Type w} [group G] (x y : G) :
nhds (x * y) = nhds x * nhds y
theorem nhds_add {G : Type w} [add_group G] (x y : G) :
nhds (x + y) = nhds x + nhds y
@[simp]
theorem nhds_mul_hom_apply {G : Type w} [group G] (a : G) :
(filter G)

On an additive topological group, `𝓝 : G → filter G` can be promoted to an `add_hom`.

Equations
@[simp]
theorem nhds_add_hom_apply {G : Type w} [add_group G] (a : G) :
def nhds_mul_hom {G : Type w} [group G]  :

On a topological group, `𝓝 : G → filter G` can be promoted to a `mul_hom`.

Equations
@[protected, instance]