# Documentation

Mathlib.Topology.Algebra.Group.Basic

# Topological groups #

This file defines the following typeclasses:

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

• ContinuousSub G means that G has a continuous subtraction operation.

There is an instance deducing ContinuousSub from TopologicalGroup 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 Equivs: Homeomorph.mulLeft, Homeomorph.mulRight, 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 (*).

theorem Homeomorph.addLeft.proof_1 {G : Type u_1} [] [] [] (a : G) :
Continuous fun x => ↑(toAddUnits a) + x
theorem Homeomorph.addLeft.proof_2 {G : Type u_1} [] [] [] (a : G) :
Continuous fun x => ↑(-toAddUnits a) + x
def Homeomorph.addLeft {G : Type w} [] [] [] (a : G) :
G ≃ₜ G

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

Instances For
def Homeomorph.mulLeft {G : Type w} [] [] [] (a : G) :
G ≃ₜ G

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

Instances For
@[simp]
theorem Homeomorph.coe_addLeft {G : Type w} [] [] [] (a : G) :
↑() = (fun x x_1 => x + x_1) a
@[simp]
theorem Homeomorph.coe_mulLeft {G : Type w} [] [] [] (a : G) :
↑() = (fun x x_1 => x * x_1) a
theorem Homeomorph.addLeft_symm {G : Type w} [] [] [] (a : G) :
theorem Homeomorph.mulLeft_symm {G : Type w} [] [] [] (a : G) :
theorem isOpenMap_add_left {G : Type w} [] [] [] (a : G) :
IsOpenMap fun x => a + x
theorem isOpenMap_mul_left {G : Type w} [] [] [] (a : G) :
IsOpenMap fun x => a * x
theorem IsOpen.left_addCoset {G : Type w} [] [] [] {U : Set G} (h : ) (x : G) :
theorem IsOpen.leftCoset {G : Type w} [] [] [] {U : Set G} (h : ) (x : G) :
theorem isClosedMap_add_left {G : Type w} [] [] [] (a : G) :
IsClosedMap fun x => a + x
theorem isClosedMap_mul_left {G : Type w} [] [] [] (a : G) :
IsClosedMap fun x => a * x
theorem IsClosed.left_addCoset {G : Type w} [] [] [] {U : Set G} (h : ) (x : G) :
theorem IsClosed.leftCoset {G : Type w} [] [] [] {U : Set G} (h : ) (x : G) :
theorem Homeomorph.addRight.proof_2 {G : Type u_1} [] [] [] (a : G) :
Continuous fun x => id x + ↑(-toAddUnits a)
def Homeomorph.addRight {G : Type w} [] [] [] (a : G) :
G ≃ₜ G

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

Instances For
theorem Homeomorph.addRight.proof_1 {G : Type u_1} [] [] [] (a : G) :
Continuous fun x => id x + ↑(toAddUnits a)
def Homeomorph.mulRight {G : Type w} [] [] [] (a : G) :
G ≃ₜ G

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

Instances For
@[simp]
theorem Homeomorph.coe_addRight {G : Type w} [] [] [] (a : G) :
↑() = fun g => g + a
@[simp]
theorem Homeomorph.coe_mulRight {G : Type w} [] [] [] (a : G) :
↑() = fun g => g * a
theorem Homeomorph.addRight_symm {G : Type w} [] [] [] (a : G) :
theorem Homeomorph.mulRight_symm {G : Type w} [] [] [] (a : G) :
theorem isOpenMap_add_right {G : Type w} [] [] [] (a : G) :
IsOpenMap fun x => x + a
theorem isOpenMap_mul_right {G : Type w} [] [] [] (a : G) :
IsOpenMap fun x => x * a
theorem IsOpen.right_addCoset {G : Type w} [] [] [] {U : Set G} (h : ) (x : G) :
theorem IsOpen.rightCoset {G : Type w} [] [] [] {U : Set G} (h : ) (x : G) :
theorem isClosedMap_add_right {G : Type w} [] [] [] (a : G) :
IsClosedMap fun x => x + a
theorem isClosedMap_mul_right {G : Type w} [] [] [] (a : G) :
IsClosedMap fun x => x * a
theorem IsClosed.right_addCoset {G : Type w} [] [] [] {U : Set G} (h : ) (x : G) :
theorem IsClosed.rightCoset {G : Type w} [] [] [] {U : Set G} (h : ) (x : G) :
theorem discreteTopology_of_open_singleton_zero {G : Type w} [] [] [] (h : IsOpen {0}) :
theorem discreteTopology_of_open_singleton_one {G : Type w} [] [] [] (h : IsOpen {1}) :

### ContinuousInv and ContinuousNeg#

class ContinuousNeg (G : Type u) [] [Neg G] :

Basic hypothesis to talk about a topological additive group. A topological additive group over M, for example, is obtained by requiring the instances AddGroup M and ContinuousAdd M and ContinuousNeg M.

Instances
class ContinuousInv (G : Type u) [] [Inv G] :

Basic hypothesis to talk about a topological group. A topological group over M, for example, is obtained by requiring the instances Group M and ContinuousMul M and ContinuousInv M.

Instances
theorem continuousOn_neg {G : Type w} [] [Neg G] [] {s : Set G} :
ContinuousOn Neg.neg s
theorem continuousOn_inv {G : Type w} [] [Inv G] [] {s : Set G} :
ContinuousOn Inv.inv s
theorem continuousWithinAt_neg {G : Type w} [] [Neg G] [] {s : Set G} {x : G} :
ContinuousWithinAt Neg.neg s x
theorem continuousWithinAt_inv {G : Type w} [] [Inv G] [] {s : Set G} {x : G} :
ContinuousWithinAt Inv.inv s x
theorem continuousAt_neg {G : Type w} [] [Neg G] [] {x : G} :
ContinuousAt Neg.neg x
theorem continuousAt_inv {G : Type w} [] [Inv G] [] {x : G} :
ContinuousAt Inv.inv x
theorem tendsto_neg {G : Type w} [] [Neg G] [] (a : G) :
Filter.Tendsto Neg.neg (nhds a) (nhds (-a))
theorem tendsto_inv {G : Type w} [] [Inv G] [] (a : G) :
Filter.Tendsto Inv.inv (nhds a) ()
theorem Filter.Tendsto.neg {α : Type u} {G : Type w} [] [Neg G] [] {f : αG} {l : } {y : G} (h : Filter.Tendsto f l (nhds y)) :
Filter.Tendsto (fun 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.

theorem Filter.Tendsto.inv {α : Type u} {G : Type w} [] [Inv G] [] {f : αG} {l : } {y : G} (h : Filter.Tendsto f l (nhds y)) :
Filter.Tendsto (fun x => (f x)⁻¹) l ()

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 Continuous.neg {α : Type u} {G : Type w} [] [Neg G] [] [] {f : αG} (hf : ) :
Continuous fun x => -f x
theorem Continuous.inv {α : Type u} {G : Type w} [] [Inv G] [] [] {f : αG} (hf : ) :
Continuous fun x => (f x)⁻¹
theorem ContinuousAt.neg {α : Type u} {G : Type w} [] [Neg G] [] [] {f : αG} {x : α} (hf : ) :
ContinuousAt (fun x => -f x) x
theorem ContinuousAt.inv {α : Type u} {G : Type w} [] [Inv G] [] [] {f : αG} {x : α} (hf : ) :
ContinuousAt (fun x => (f x)⁻¹) x
theorem ContinuousOn.neg {α : Type u} {G : Type w} [] [Neg G] [] [] {f : αG} {s : Set α} (hf : ) :
ContinuousOn (fun x => -f x) s
theorem ContinuousOn.inv {α : Type u} {G : Type w} [] [Inv G] [] [] {f : αG} {s : Set α} (hf : ) :
ContinuousOn (fun x => (f x)⁻¹) s
theorem ContinuousWithinAt.neg {α : Type u} {G : Type w} [] [Neg G] [] [] {f : αG} {s : Set α} {x : α} (hf : ) :
ContinuousWithinAt (fun x => -f x) s x
theorem ContinuousWithinAt.inv {α : Type u} {G : Type w} [] [Inv G] [] [] {f : αG} {s : Set α} {x : α} (hf : ) :
ContinuousWithinAt (fun x => (f x)⁻¹) s x
instance Prod.continuousNeg {G : Type w} {H : Type x} [] [Neg G] [] [] [Neg H] [] :
theorem Prod.continuousNeg.proof_1 {G : Type u_1} {H : Type u_2} [] [Neg G] [] [] [Neg H] [] :
instance Prod.continuousInv {G : Type w} {H : Type x} [] [Inv G] [] [] [Inv H] [] :
theorem Pi.continuousNeg.proof_1 {ι : Type u_1} {C : ιType u_2} [(i : ι) → TopologicalSpace (C i)] [(i : ι) → Neg (C i)] [∀ (i : ι), ContinuousNeg (C i)] :
ContinuousNeg ((i : ι) → C i)
instance Pi.continuousNeg {ι : Type u_1} {C : ιType u_2} [(i : ι) → TopologicalSpace (C i)] [(i : ι) → Neg (C i)] [∀ (i : ι), ContinuousNeg (C i)] :
ContinuousNeg ((i : ι) → C i)
instance Pi.continuousInv {ι : Type u_1} {C : ιType u_2} [(i : ι) → TopologicalSpace (C i)] [(i : ι) → Inv (C i)] [∀ (i : ι), ContinuousInv (C i)] :
ContinuousInv ((i : ι) → C i)
instance Pi.has_continuous_neg' {G : Type w} [] [Neg G] [] {ι : Type u_1} :
ContinuousNeg (ιG)

A version of Pi.continuousNeg for non-dependent functions. It is needed because sometimes Lean fails to use Pi.continuousNeg for non-dependent functions.

theorem Pi.has_continuous_neg'.proof_1 {G : Type u_1} [] [Neg G] [] {ι : Type u_2} :
ContinuousNeg (ιG)
instance Pi.has_continuous_inv' {G : Type w} [] [Inv G] [] {ι : Type u_1} :
ContinuousInv (ιG)

A version of Pi.continuousInv for non-dependent functions. It is needed because sometimes Lean fails to use Pi.continuousInv for non-dependent functions.

instance continuousNeg_of_discreteTopology {H : Type x} [] [Neg H] [] :
instance continuousInv_of_discreteTopology {H : Type x} [] [Inv H] [] :
theorem isClosed_setOf_map_neg (G₁ : Type u_2) (G₂ : Type u_3) [] [T2Space G₂] [Neg G₁] [Neg G₂] [] :
IsClosed {f | ∀ (x : G₁), f (-x) = -f x}
theorem isClosed_setOf_map_inv (G₁ : Type u_2) (G₂ : Type u_3) [] [T2Space G₂] [Inv G₁] [Inv G₂] [] :
IsClosed {f | ∀ (x : G₁), f x⁻¹ = (f x)⁻¹}
theorem IsCompact.neg {G : Type w} [] [] [] {s : Set G} (hs : ) :
theorem IsCompact.inv {G : Type w} [] [] [] {s : Set G} (hs : ) :
def Homeomorph.neg (G : Type u_1) [] [] [] :
G ≃ₜ G

Negation in a topological group as a homeomorphism.

Instances For
theorem Homeomorph.neg.proof_1 (G : Type u_1) [] [] [] :
Continuous fun a => -a
def Homeomorph.inv (G : Type u_1) [] [] [] :
G ≃ₜ G

Inversion in a topological group as a homeomorphism.

Instances For
theorem isOpenMap_neg (G : Type w) [] [] [] :
IsOpenMap Neg.neg
theorem isOpenMap_inv (G : Type w) [] [] [] :
IsOpenMap Inv.inv
theorem isClosedMap_neg (G : Type w) [] [] [] :
IsClosedMap Neg.neg
theorem isClosedMap_inv (G : Type w) [] [] [] :
IsClosedMap Inv.inv
theorem IsOpen.neg {G : Type w} [] [] [] {s : Set G} (hs : ) :
theorem IsOpen.inv {G : Type w} [] [] [] {s : Set G} (hs : ) :
theorem IsClosed.neg {G : Type w} [] [] [] {s : Set G} (hs : ) :
theorem IsClosed.inv {G : Type w} [] [] [] {s : Set G} (hs : ) :
theorem neg_closure {G : Type w} [] [] [] (s : Set G) :
theorem inv_closure {G : Type w} [] [] [] (s : Set G) :
()⁻¹ =
theorem continuousNeg_sInf {G : Type w} [Neg G] {ts : } (h : ∀ (t : ), t ts) :
theorem continuousInv_sInf {G : Type w} [Inv G] {ts : } (h : ∀ (t : ), t ts) :
theorem continuousNeg_iInf {G : Type w} {ι' : Sort u_1} [Neg G] {ts' : ι'} (h' : ∀ (i : ι'), ) :
theorem continuousInv_iInf {G : Type w} {ι' : Sort u_1} [Inv G] {ts' : ι'} (h' : ∀ (i : ι'), ) :
theorem continuousNeg_inf {G : Type w} [Neg G] {t₁ : } {t₂ : } (h₁ : ) (h₂ : ) :
theorem continuousInv_inf {G : Type w} [Inv G] {t₁ : } {t₂ : } (h₁ : ) (h₂ : ) :
theorem Inducing.continuousNeg {G : Type u_1} {H : Type u_2} [Neg G] [Neg H] [] [] [] {f : GH} (hf : ) (hf_inv : ∀ (x : G), f (-x) = -f x) :
theorem Inducing.continuousInv {G : Type u_1} {H : Type u_2} [Inv G] [Inv H] [] [] [] {f : GH} (hf : ) (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 TopologicalAddGroup (G : Type u) [] [] extends , :

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

Instances
class TopologicalGroup (G : Type u_1) [] [] extends , :

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 UniformSpace instance, you should also provide an instance of UniformSpace and UniformGroup using TopologicalGroup.toUniformSpace and topologicalCommGroup_isUniform.

Instances
instance ConjAct.units_continuousConstSMul {M : Type u_1} [] [] [] :
theorem TopologicalAddGroup.continuous_conj_sum {G : Type w} [] [Neg G] [Add G] [] [] :
Continuous fun g => g.fst + g.snd + -g.fst

Conjugation is jointly continuous on G × G when both add and neg are continuous.

theorem TopologicalGroup.continuous_conj_prod {G : Type w} [] [Inv G] [Mul G] [] [] :
Continuous fun g => g.fst * g.snd * g.fst⁻¹

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

theorem TopologicalAddGroup.continuous_conj {G : Type w} [] [Neg G] [Add G] [] (g : G) :
Continuous fun h => g + h + -g

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

theorem TopologicalGroup.continuous_conj {G : Type w} [] [Inv G] [Mul G] [] (g : G) :
Continuous fun h => g * h * g⁻¹

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

theorem TopologicalAddGroup.continuous_conj' {G : Type w} [] [Neg G] [Add G] [] [] (h : G) :
Continuous fun g => g + h + -g

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

theorem TopologicalGroup.continuous_conj' {G : Type w} [] [Inv G] [Mul G] [] [] (h : G) :
Continuous fun g => g * h * g⁻¹

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

theorem continuous_zsmul {G : Type w} [] [] (z : ) :
Continuous fun a => z a
abbrev continuous_zsmul.match_1 (motive : ) :
(x : ) → ((n : ) → motive ()) → ((n : ) → motive ()) → motive x
Instances For
theorem continuous_zpow {G : Type w} [] [] [] (z : ) :
Continuous fun a => a ^ z
instance AddGroup.continuousConstSMul_int {A : Type u_1} [] [] :
instance AddGroup.continuousSMul_int {A : Type u_1} [] [] :
theorem Continuous.zsmul {α : Type u} {G : Type w} [] [] [] {f : αG} (h : ) (z : ) :
Continuous fun b => z f b
theorem Continuous.zpow {α : Type u} {G : Type w} [] [] [] [] {f : αG} (h : ) (z : ) :
Continuous fun b => f b ^ z
theorem continuousOn_zsmul {G : Type w} [] [] {s : Set G} (z : ) :
ContinuousOn (fun x => z x) s
theorem continuousOn_zpow {G : Type w} [] [] [] {s : Set G} (z : ) :
ContinuousOn (fun x => x ^ z) s
theorem continuousAt_zsmul {G : Type w} [] [] (x : G) (z : ) :
ContinuousAt (fun x => z x) x
theorem continuousAt_zpow {G : Type w} [] [] [] (x : G) (z : ) :
ContinuousAt (fun x => x ^ z) x
theorem Filter.Tendsto.zsmul {G : Type w} [] [] {α : Type u_1} {l : } {f : αG} {x : G} (hf : Filter.Tendsto f l (nhds x)) (z : ) :
Filter.Tendsto (fun x => z f x) l (nhds (z x))
theorem Filter.Tendsto.zpow {G : Type w} [] [] [] {α : Type u_1} {l : } {f : αG} {x : G} (hf : Filter.Tendsto f l (nhds x)) (z : ) :
Filter.Tendsto (fun x => f x ^ z) l (nhds (x ^ z))
theorem ContinuousWithinAt.zsmul {α : Type u} {G : Type w} [] [] [] {f : αG} {x : α} {s : Set α} (hf : ) (z : ) :
ContinuousWithinAt (fun x => z f x) s x
theorem ContinuousWithinAt.zpow {α : Type u} {G : Type w} [] [] [] [] {f : αG} {x : α} {s : Set α} (hf : ) (z : ) :
ContinuousWithinAt (fun x => f x ^ z) s x
theorem ContinuousAt.zsmul {α : Type u} {G : Type w} [] [] [] {f : αG} {x : α} (hf : ) (z : ) :
ContinuousAt (fun x => z f x) x
theorem ContinuousAt.zpow {α : Type u} {G : Type w} [] [] [] [] {f : αG} {x : α} (hf : ) (z : ) :
ContinuousAt (fun x => f x ^ z) x
theorem ContinuousOn.zsmul {α : Type u} {G : Type w} [] [] [] {f : αG} {s : Set α} (hf : ) (z : ) :
ContinuousOn (fun x => z f x) s
theorem ContinuousOn.zpow {α : Type u} {G : Type w} [] [] [] [] {f : αG} {s : Set α} (hf : ) (z : ) :
ContinuousOn (fun x => f x ^ z) s
theorem tendsto_neg_nhdsWithin_Ioi {H : Type x} [] [] {a : H} :
Filter.Tendsto Neg.neg (nhdsWithin a ()) (nhdsWithin (-a) (Set.Iio (-a)))
theorem tendsto_inv_nhdsWithin_Ioi {H : Type x} [] [] [] {a : H} :
Filter.Tendsto Inv.inv (nhdsWithin a ()) ()
theorem tendsto_neg_nhdsWithin_Iio {H : Type x} [] [] {a : H} :
Filter.Tendsto Neg.neg (nhdsWithin a ()) (nhdsWithin (-a) (Set.Ioi (-a)))
theorem tendsto_inv_nhdsWithin_Iio {H : Type x} [] [] [] {a : H} :
Filter.Tendsto Inv.inv (nhdsWithin a ()) ()
theorem tendsto_neg_nhdsWithin_Ioi_neg {H : Type x} [] [] {a : H} :
Filter.Tendsto Neg.neg (nhdsWithin (-a) (Set.Ioi (-a))) (nhdsWithin a ())
theorem tendsto_inv_nhdsWithin_Ioi_inv {H : Type x} [] [] [] {a : H} :
Filter.Tendsto Inv.inv () (nhdsWithin a ())
theorem tendsto_neg_nhdsWithin_Iio_neg {H : Type x} [] [] {a : H} :
Filter.Tendsto Neg.neg (nhdsWithin (-a) (Set.Iio (-a))) (nhdsWithin a ())
theorem tendsto_inv_nhdsWithin_Iio_inv {H : Type x} [] [] [] {a : H} :
Filter.Tendsto Inv.inv () (nhdsWithin a ())
theorem tendsto_neg_nhdsWithin_Ici {H : Type x} [] [] {a : H} :
Filter.Tendsto Neg.neg (nhdsWithin a ()) (nhdsWithin (-a) (Set.Iic (-a)))
theorem tendsto_inv_nhdsWithin_Ici {H : Type x} [] [] [] {a : H} :
Filter.Tendsto Inv.inv (nhdsWithin a ()) ()
theorem tendsto_neg_nhdsWithin_Iic {H : Type x} [] [] {a : H} :
Filter.Tendsto Neg.neg (nhdsWithin a ()) (nhdsWithin (-a) (Set.Ici (-a)))
theorem tendsto_inv_nhdsWithin_Iic {H : Type x} [] [] [] {a : H} :
Filter.Tendsto Inv.inv (nhdsWithin a ()) ()
theorem tendsto_neg_nhdsWithin_Ici_neg {H : Type x} [] [] {a : H} :
Filter.Tendsto Neg.neg (nhdsWithin (-a) (Set.Ici (-a))) (nhdsWithin a ())
theorem tendsto_inv_nhdsWithin_Ici_inv {H : Type x} [] [] [] {a : H} :
Filter.Tendsto Inv.inv () (nhdsWithin a ())
theorem tendsto_neg_nhdsWithin_Iic_neg {H : Type x} [] [] {a : H} :
Filter.Tendsto Neg.neg (nhdsWithin (-a) (Set.Iic (-a))) (nhdsWithin a ())
theorem tendsto_inv_nhdsWithin_Iic_inv {H : Type x} [] [] [] {a : H} :
Filter.Tendsto Inv.inv () (nhdsWithin a ())
theorem Pi.topologicalAddGroup.proof_1 {β : Type u_1} {C : βType u_2} [(b : β) → TopologicalSpace (C b)] [(b : β) → AddGroup (C b)] [∀ (b : β), TopologicalAddGroup (C b)] :
TopologicalAddGroup ((b : β) → C b)
instance Pi.topologicalAddGroup {β : Type v} {C : βType u_1} [(b : β) → TopologicalSpace (C b)] [(b : β) → AddGroup (C b)] [∀ (b : β), TopologicalAddGroup (C b)] :
TopologicalAddGroup ((b : β) → C b)
instance Pi.topologicalGroup {β : Type v} {C : βType u_1} [(b : β) → TopologicalSpace (C b)] [(b : β) → Group (C b)] [∀ (b : β), TopologicalGroup (C b)] :
TopologicalGroup ((b : β) → C b)

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

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

theorem nhds_zero_symm (G : Type w) [] [] :
Filter.comap Neg.neg (nhds 0) = nhds 0
theorem nhds_one_symm (G : Type w) [] [] [] :
Filter.comap Inv.inv (nhds 1) = nhds 1
theorem nhds_zero_symm' (G : Type w) [] [] :
Filter.map Neg.neg (nhds 0) = nhds 0
theorem nhds_one_symm' (G : Type w) [] [] [] :
Filter.map Inv.inv (nhds 1) = nhds 1
theorem neg_mem_nhds_zero (G : Type w) [] [] {S : Set G} (hS : S nhds 0) :
theorem inv_mem_nhds_one (G : Type w) [] [] [] {S : Set G} (hS : S nhds 1) :
theorem Homeomorph.shearAddRight.proof_1 (G : Type u_1) [] :
def Homeomorph.shearAddRight (G : Type w) [] [] :
G × G ≃ₜ G × G

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

Instances For
theorem Homeomorph.shearAddRight.proof_3 (G : Type u_1) [] [] :
Continuous fun x => (x.fst, ↑(Equiv.addLeft x.fst) x.snd)
theorem Homeomorph.shearAddRight.proof_4 (G : Type u_1) [] [] :
Continuous fun x => (x.fst, (Equiv.addLeft (().symm x.fst)).symm x.snd)
theorem Homeomorph.shearAddRight.proof_2 (G : Type u_1) [] :
def Homeomorph.shearMulRight (G : Type w) [] [] [] :
G × G ≃ₜ G × G

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

Instances For
@[simp]
theorem Homeomorph.shearAddRight_coe (G : Type w) [] [] :
= fun z => (z.fst, z.fst + z.snd)
@[simp]
theorem Homeomorph.shearMulRight_coe (G : Type w) [] [] [] :
= fun z => (z.fst, z.fst * z.snd)
@[simp]
theorem Homeomorph.shearAddRight_symm_coe (G : Type w) [] [] :
= fun z => (z.fst, -z.fst + z.snd)
@[simp]
theorem Homeomorph.shearMulRight_symm_coe (G : Type w) [] [] [] :
= fun z => (z.fst, z.fst⁻¹ * z.snd)
theorem Inducing.topologicalAddGroup {G : Type w} {H : Type x} [] [] {F : Type u_1} [] [] [] (f : F) (hf : Inducing f) :
theorem Inducing.topologicalGroup {G : Type w} {H : Type x} [] [] [] {F : Type u_1} [] [] [] (f : F) (hf : Inducing f) :
theorem topologicalAddGroup_induced {G : Type w} {H : Type x} [] [] {F : Type u_1} [] [] (f : F) :
theorem topologicalGroup_induced {G : Type w} {H : Type x} [] [] [] {F : Type u_1} [] [] (f : F) :
theorem AddSubgroup.topologicalClosure.proof_1 {G : Type u_1} [] [] (s : ) :
def AddSubgroup.topologicalClosure {G : Type w} [] [] (s : ) :

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

Instances For
theorem AddSubgroup.topologicalClosure.proof_2 {G : Type u_1} [] [] (s : ) :
def Subgroup.topologicalClosure {G : Type w} [] [] [] (s : ) :

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

Instances For
@[simp]
theorem AddSubgroup.topologicalClosure_coe {G : Type w} [] [] {s : } :
@[simp]
theorem Subgroup.topologicalClosure_coe {G : Type w} [] [] [] {s : } :
theorem AddSubgroup.le_topologicalClosure {G : Type w} [] [] (s : ) :
theorem Subgroup.le_topologicalClosure {G : Type w} [] [] [] (s : ) :
theorem Subgroup.isClosed_topologicalClosure {G : Type w} [] [] [] (s : ) :
theorem AddSubgroup.topologicalClosure_minimal {G : Type w} [] [] (s : ) {t : } (h : s t) (ht : IsClosed t) :
theorem Subgroup.topologicalClosure_minimal {G : Type w} [] [] [] (s : ) {t : } (h : s t) (ht : IsClosed t) :
theorem DenseRange.topologicalClosure_map_addSubgroup {G : Type w} {H : Type x} [] [] [] [] {f : G →+ H} (hf : ) (hf' : ) {s : } (hs : ) :
theorem DenseRange.topologicalClosure_map_subgroup {G : Type w} {H : Type x} [] [] [] [] [] [] {f : G →* H} (hf : ) (hf' : ) {s : } (hs : ) :
theorem AddSubgroup.is_normal_topologicalClosure {G : Type u_1} [] [] (N : ) :

The topological closure of a normal additive subgroup is normal.

theorem Subgroup.is_normal_topologicalClosure {G : Type u_1} [] [] [] (N : ) [] :

The topological closure of a normal subgroup is normal.

theorem add_mem_connectedComponent_zero {G : Type u_1} [] [] [] {g : G} {h : G} (hg : ) (hh : ) :
g + h
theorem mul_mem_connectedComponent_one {G : Type u_1} [] [] [] {g : G} {h : G} (hg : ) (hh : ) :
g * h
theorem neg_mem_connectedComponent_zero {G : Type u_1} [] [] {g : G} (hg : ) :
theorem inv_mem_connectedComponent_one {G : Type u_1} [] [] [] {g : G} (hg : ) :
theorem AddSubgroup.connectedComponentOfZero.proof_1 (G : Type u_1) [] [] :
∀ {a b : G}, a + b

The connected component of 0 is a subgroup of G.

Instances For
def Subgroup.connectedComponentOfOne (G : Type u_1) [] [] [] :

The connected component of 1 is a subgroup of G.

Instances For
def AddSubgroup.addCommGroupTopologicalClosure {G : Type w} [] [] [] (s : ) (hs : ∀ (x y : { x // x s }), x + y = y + x) :

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

Instances For
theorem AddSubgroup.addCommGroupTopologicalClosure.proof_1 {G : Type u_1} [] [] (s : ) (a : { x // }) :
-a + a = 0
theorem AddSubgroup.addCommGroupTopologicalClosure.proof_2 {G : Type u_1} [] [] [] (s : ) (hs : ∀ (x y : { x // x s }), x + y = y + x) (a : { x // x AddSubmonoid.topologicalClosure s.toAddSubmonoid }) (b : { x // x AddSubmonoid.topologicalClosure s.toAddSubmonoid }) :
a + b = b + a
def Subgroup.commGroupTopologicalClosure {G : Type w} [] [] [] [] (s : ) (hs : ∀ (x y : { x // x s }), x * y = y * x) :
CommGroup { x // }

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

Instances For
theorem exists_nhds_half_neg {G : Type w} [] [] {s : Set G} (hs : s nhds 0) :
V, V nhds 0 ∀ (v : G), v V∀ (w : G), w Vv - w s
theorem exists_nhds_split_inv {G : Type w} [] [] [] {s : Set G} (hs : s nhds 1) :
V, V nhds 1 ∀ (v : G), v V∀ (w : G), w Vv / w s
theorem nhds_translation_add_neg {G : Type w} [] [] (x : G) :
Filter.comap (fun y => y + -x) (nhds 0) = nhds x
theorem nhds_translation_mul_inv {G : Type w} [] [] [] (x : G) :
Filter.comap (fun y => y * x⁻¹) (nhds 1) = nhds x
@[simp]
theorem map_add_left_nhds {G : Type w} [] [] (x : G) (y : G) :
Filter.map ((fun x x_1 => x + x_1) x) (nhds y) = nhds (x + y)
@[simp]
theorem map_mul_left_nhds {G : Type w} [] [] [] (x : G) (y : G) :
Filter.map ((fun x x_1 => x * x_1) x) (nhds y) = nhds (x * y)
theorem map_add_left_nhds_zero {G : Type w} [] [] (x : G) :
Filter.map ((fun x x_1 => x + x_1) x) (nhds 0) = nhds x
theorem map_mul_left_nhds_one {G : Type w} [] [] [] (x : G) :
Filter.map ((fun x x_1 => x * x_1) x) (nhds 1) = nhds x
@[simp]
theorem map_add_right_nhds {G : Type w} [] [] (x : G) (y : G) :
Filter.map (fun z => z + x) (nhds y) = nhds (y + x)
@[simp]
theorem map_mul_right_nhds {G : Type w} [] [] [] (x : G) (y : G) :
Filter.map (fun z => z * x) (nhds y) = nhds (y * x)
theorem map_add_right_nhds_zero {G : Type w} [] [] (x : G) :
Filter.map (fun y => y + x) (nhds 0) = nhds x
theorem map_mul_right_nhds_one {G : Type w} [] [] [] (x : G) :
Filter.map (fun y => y * x) (nhds 1) = nhds x
theorem Filter.HasBasis.nhds_of_zero {G : Type w} [] [] {ι : Sort u_1} {p : ιProp} {s : ιSet G} (hb : Filter.HasBasis (nhds 0) p s) (x : G) :
Filter.HasBasis (nhds x) p fun i => {y | y - x s i}
theorem Filter.HasBasis.nhds_of_one {G : Type w} [] [] [] {ι : Sort u_1} {p : ιProp} {s : ιSet G} (hb : Filter.HasBasis (nhds 1) p s) (x : G) :
Filter.HasBasis (nhds x) p fun i => {y | y / x s i}
theorem mem_closure_iff_nhds_zero {G : Type w} [] [] {x : G} {s : Set G} :
x ∀ (U : Set G), U nhds 0y, y s y - x U
theorem mem_closure_iff_nhds_one {G : Type w} [] [] [] {x : G} {s : Set G} :
x ∀ (U : Set G), U nhds 1y, y s y / x U
theorem continuous_of_continuousAt_zero {G : Type w} [] [] {M : Type u_1} {hom : Type u_2} [] [] [] [AddMonoidHomClass hom G M] (f : hom) (hf : ContinuousAt (f) 0) :

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

theorem continuous_of_continuousAt_one {G : Type w} [] [] [] {M : Type u_1} {hom : Type u_2} [] [] [] [MonoidHomClass hom G M] (f : hom) (hf : ContinuousAt (f) 1) :

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

abbrev continuous_of_continuousAt_zero₂.match_1 {G : Type u_1} {H : Type u_2} (motive : G × HProp) :
(x : G × H) → ((x : G) → (y : H) → motive (x, y)) → motive x
Instances For
theorem continuous_of_continuousAt_zero₂ {G : Type w} [] [] {H : Type u_1} {M : Type u_2} [] [] [] [] [] (f : G →+ H →+ M) (hf : ContinuousAt (fun x => ↑(f x.fst) x.snd) (0, 0)) (hl : ∀ (x : G), ContinuousAt (↑(f x)) 0) (hr : ∀ (y : H), ContinuousAt (fun x => ↑(f x) y) 0) :
Continuous fun x => ↑(f x.fst) x.snd
theorem continuous_of_continuousAt_one₂ {G : Type w} [] [] [] {H : Type u_1} {M : Type u_2} [] [] [] [] [] [] (f : G →* H →* M) (hf : ContinuousAt (fun x => ↑(f x.fst) x.snd) (1, 1)) (hl : ∀ (x : G), ContinuousAt (↑(f x)) 1) (hr : ∀ (y : H), ContinuousAt (fun x => ↑(f x) y) 1) :
Continuous fun x => ↑(f x.fst) x.snd
theorem TopologicalAddGroup.ext {G : Type u_1} [] {t : } {t' : } (tg : ) (tg' : ) (h : nhds 0 = nhds 0) :
t = t'
theorem TopologicalGroup.ext {G : Type u_1} [] {t : } {t' : } (tg : ) (tg' : ) (h : nhds 1 = nhds 1) :
t = t'
theorem TopologicalAddGroup.ext_iff {G : Type u_1} [] {t : } {t' : } (tg : ) (tg' : ) :
t = t' nhds 0 = nhds 0
theorem TopologicalGroup.ext_iff {G : Type u_1} [] {t : } {t' : } (tg : ) (tg' : ) :
t = t' nhds 1 = nhds 1
theorem ContinuousNeg.of_nhds_zero {G : Type u_1} [] [] (hinv : Filter.Tendsto (fun x => -x) (nhds 0) (nhds 0)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun x => x₀ + x) (nhds 0)) (hconj : ∀ (x₀ : G), Filter.Tendsto (fun x => x₀ + x + -x₀) (nhds 0) (nhds 0)) :
theorem ContinuousInv.of_nhds_one {G : Type u_1} [] [] (hinv : Filter.Tendsto (fun x => x⁻¹) (nhds 1) (nhds 1)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun x => x₀ * x) (nhds 1)) (hconj : ∀ (x₀ : G), Filter.Tendsto (fun x => x₀ * x * x₀⁻¹) (nhds 1) (nhds 1)) :
theorem TopologicalAddGroup.of_nhds_zero' {G : Type u} [] [] (hmul : Filter.Tendsto (Function.uncurry fun x x_1 => x + x_1) (nhds 0 ×ˢ nhds 0) (nhds 0)) (hinv : Filter.Tendsto (fun x => -x) (nhds 0) (nhds 0)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun x => x₀ + x) (nhds 0)) (hright : ∀ (x₀ : G), nhds x₀ = Filter.map (fun x => x + x₀) (nhds 0)) :
theorem TopologicalGroup.of_nhds_one' {G : Type u} [] [] (hmul : Filter.Tendsto (Function.uncurry fun x x_1 => x * x_1) (nhds 1 ×ˢ nhds 1) (nhds 1)) (hinv : Filter.Tendsto (fun x => x⁻¹) (nhds 1) (nhds 1)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun x => x₀ * x) (nhds 1)) (hright : ∀ (x₀ : G), nhds x₀ = Filter.map (fun x => x * x₀) (nhds 1)) :
theorem TopologicalAddGroup.of_nhds_zero {G : Type u} [] [] (hmul : Filter.Tendsto (Function.uncurry fun x x_1 => x + x_1) (nhds 0 ×ˢ nhds 0) (nhds 0)) (hinv : Filter.Tendsto (fun x => -x) (nhds 0) (nhds 0)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun x => x₀ + x) (nhds 0)) (hconj : ∀ (x₀ : G), Filter.Tendsto (fun x => x₀ + x + -x₀) (nhds 0) (nhds 0)) :
theorem TopologicalGroup.of_nhds_one {G : Type u} [] [] (hmul : Filter.Tendsto (Function.uncurry fun x x_1 => x * x_1) (nhds 1 ×ˢ nhds 1) (nhds 1)) (hinv : Filter.Tendsto (fun x => x⁻¹) (nhds 1) (nhds 1)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun x => x₀ * x) (nhds 1)) (hconj : ∀ (x₀ : G), Filter.Tendsto (fun x => x₀ * x * x₀⁻¹) (nhds 1) (nhds 1)) :
theorem TopologicalAddGroup.of_comm_of_nhds_zero {G : Type u} [] [] (hmul : Filter.Tendsto (Function.uncurry fun x x_1 => x + x_1) (nhds 0 ×ˢ nhds 0) (nhds 0)) (hinv : Filter.Tendsto (fun x => -x) (nhds 0) (nhds 0)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun x => x₀ + x) (nhds 0)) :
theorem TopologicalGroup.of_comm_of_nhds_one {G : Type u} [] [] (hmul : Filter.Tendsto (Function.uncurry fun x x_1 => x * x_1) (nhds 1 ×ˢ nhds 1) (nhds 1)) (hinv : Filter.Tendsto (fun x => x⁻¹) (nhds 1) (nhds 1)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun x => x₀ * x) (nhds 1)) :
theorem QuotientAddGroup.isOpenMap_coe {G : Type w} [] [] (N : ) :
theorem QuotientGroup.isOpenMap_coe {G : Type w} [] [] [] (N : ) :
IsOpenMap QuotientGroup.mk
instance topologicalAddGroup_quotient {G : Type w} [] [] (N : ) :
instance topologicalGroup_quotient {G : Type w} [] [] [] (N : ) [] :
theorem QuotientAddGroup.nhds_eq {G : Type w} [] [] (N : ) (x : G) :
nhds x = Filter.map QuotientAddGroup.mk (nhds x)

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

theorem QuotientGroup.nhds_eq {G : Type w} [] [] [] (N : ) (x : G) :
nhds x = Filter.map QuotientGroup.mk (nhds x)

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

theorem TopologicalAddGroup.exists_antitone_basis_nhds_zero (G : Type w) [] [] :
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 QuotientAddGroup.completeSpace

theorem TopologicalGroup.exists_antitone_basis_nhds_one (G : Type w) [] [] [] :
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 QuotientGroup.completeSpace

instance QuotientAddGroup.nhds_zero_isCountablyGenerated (G : Type w) [] [] (N : ) (n : ) :

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

instance QuotientGroup.nhds_one_isCountablyGenerated (G : Type w) [] [] [] (N : ) (n : ) :

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

class ContinuousSub (G : Type u_1) [] [Sub G] :

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
class ContinuousDiv (G : Type u_1) [] [Div G] :

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 GroupWithZero.

Instances
instance TopologicalGroup.to_continuousDiv {G : Type w} [] [] [] :
theorem Filter.Tendsto.sub {α : Type u} {G : Type w} [] [Sub G] [] {f : αG} {g : αG} {l : } {a : G} {b : G} (hf : Filter.Tendsto f l (nhds a)) (hg : Filter.Tendsto g l (nhds b)) :
Filter.Tendsto (fun x => f x - g x) l (nhds (a - b))
theorem Filter.Tendsto.div' {α : Type u} {G : Type w} [] [Div G] [] {f : αG} {g : αG} {l : } {a : G} {b : G} (hf : Filter.Tendsto f l (nhds a)) (hg : Filter.Tendsto g l (nhds b)) :
Filter.Tendsto (fun x => f x / g x) l (nhds (a / b))
theorem Filter.Tendsto.const_sub {α : Type u} {G : Type w} [] [Sub G] [] (b : G) {c : G} {f : αG} {l : } (h : Filter.Tendsto f l (nhds c)) :
Filter.Tendsto (fun k => b - f k) l (nhds (b - c))
theorem Filter.Tendsto.const_div' {α : Type u} {G : Type w} [] [Div G] [] (b : G) {c : G} {f : αG} {l : } (h : Filter.Tendsto f l (nhds c)) :
Filter.Tendsto (fun k => b / f k) l (nhds (b / c))
theorem Filter.Tendsto.sub_const {α : Type u} {G : Type w} [] [Sub G] [] {c : G} {f : αG} {l : } (h : Filter.Tendsto f l (nhds c)) (b : G) :
Filter.Tendsto (fun k => f k - b) l (nhds (c - b))
theorem Filter.Tendsto.div_const' {α : Type u} {G : Type w} [] [Div G] [] {c : G} {f : αG} {l : } (h : Filter.Tendsto f l (nhds c)) (b : G) :
Filter.Tendsto (fun k => f k / b) l (nhds (c / b))
theorem Continuous.sub {α : Type u} {G : Type w} [] [Sub G] [] [] {f : αG} {g : αG} (hf : ) (hg : ) :
Continuous fun x => f x - g x
theorem Continuous.div' {α : Type u} {G : Type w} [] [Div G] [] [] {f : αG} {g : αG} (hf : ) (hg : ) :
Continuous fun x => f x / g x
theorem continuous_sub_left {G : Type w} [] [Sub G] [] (a : G) :
Continuous fun b => a - b
theorem continuous_div_left' {G : Type w} [] [Div G] [] (a : G) :
Continuous fun b => a / b
theorem continuous_sub_right {G : Type w} [] [Sub G] [] (a : G) :
Continuous fun b => b - a
theorem continuous_div_right' {G : Type w} [] [Div G] [] (a : G) :
Continuous fun b => b / a
theorem ContinuousAt.sub {α : Type u} {G : Type w} [] [Sub G] [] [] {f : αG} {g : αG} {x : α} (hf : ) (hg : ) :
ContinuousAt (fun x => f x - g x) x
theorem ContinuousAt.div' {α : Type u} {G : Type w} [] [Div G] [] [] {f : αG} {g : αG} {x : α} (hf : ) (hg : ) :
ContinuousAt (fun x => f x / g x) x
theorem ContinuousWithinAt.sub {α : Type u} {G : Type w} [] [Sub G] [] [] {f : αG} {g : αG} {s : Set α} {x : α} (hf : ) (hg : ) :
ContinuousWithinAt (fun x => f x - g x) s x
theorem ContinuousWithinAt.div' {α : Type u} {G : Type w} [] [Div G] [] [] {f : αG} {g : αG} {s : Set α} {x : α} (hf : ) (hg : ) :
ContinuousWithinAt (fun x => f x / g x) s x
theorem ContinuousOn.sub {α : Type u} {G : Type w} [] [Sub G] [] [] {f : αG} {g : αG} {s : Set α} (hf : ) (hg : ) :
ContinuousOn (fun x => f x - g x) s
theorem ContinuousOn.div' {α : Type u} {G : Type w} [] [Div G] [] [] {f : αG} {g : αG} {s : Set α} (hf : ) (hg : ) :
ContinuousOn (fun x => f x / g x) s
theorem Homeomorph.subLeft.proof_1 {G : Type u_1} [] [] (x : G) :
Continuous fun x => x - x
theorem Homeomorph.subLeft.proof_2 {G : Type u_1} [] [] (x : G) :
Continuous fun x => -x + x
def Homeomorph.subLeft {G : Type w} [] [] (x : G) :
G ≃ₜ G

A version of Homeomorph.addLeft a (-b) that is defeq to a - b.

Instances For
@[simp]
theorem Homeomorph.divLeft_symm_apply {G : Type w} [] [] [] (x : G) (b : G) :
↑() b = b⁻¹ * x
@[simp]
theorem Homeomorph.divLeft_apply {G : Type w} [] [] [] (x : G) (b : G) :
↑() b = x / b
@[simp]
theorem Homeomorph.subLeft_symm_apply {G : Type w} [] [] (x : G) (b : G) :
↑() b = -b + x
@[simp]
theorem Homeomorph.subLeft_apply {G : Type w} [] [] (x : G) (b : G) :
↑() b = x - b
def Homeomorph.divLeft {G : Type w} [] [] [] (x : G) :
G ≃ₜ G

A version of Homeomorph.mulLeft a b⁻¹ that is defeq to a / b.

Instances For
theorem isOpenMap_sub_left {G : Type w} [] [] (a : G) :
IsOpenMap ((fun x x_1 => x - x_1) a)
theorem isOpenMap_div_left {G : Type w} [] [] [] (a : G) :
IsOpenMap ((fun x x_1 => x / x_1) a)
theorem isClosedMap_sub_left {G : Type w} [] [] (a : G) :
IsClosedMap ((fun x x_1 => x - x_1) a)
theorem isClosedMap_div_left {G : Type w} [] [] [] (a : G) :
IsClosedMap ((fun x x_1 => x / x_1) a)
theorem Homeomorph.subRight.proof_2 {G : Type u_1} [] [] (x : G) :
Continuous fun x => id x + x
def Homeomorph.subRight {G : Type w} [] [] (x : G) :
G ≃ₜ G

A version of Homeomorph.addRight (-a) b that is defeq to b - a.

Instances For
theorem Homeomorph.subRight.proof_1 {G : Type u_1} [] [] (x : G) :
Continuous fun x => id x - x
@[simp]
theorem Homeomorph.divRight_apply {G : Type w} [] [] [] (x : G) (b : G) :
↑() b = b / x
@[simp]
theorem Homeomorph.subRight_apply {G : Type w} [] [] (x : G) (b : G) :
↑() b = b - x
@[simp]
theorem Homeomorph.divRight_symm_apply {G : Type w} [] [] [] (x : G) (b : G) :
↑() b = b * x
@[simp]
theorem Homeomorph.subRight_symm_apply {G : Type w} [] [] (x : G) (b : G) :
↑() b = b + x
def Homeomorph.divRight {G : Type w} [] [] [] (x : G) :
G ≃ₜ G

A version of Homeomorph.mulRight a⁻¹ b that is defeq to b / a.

Instances For
theorem isOpenMap_sub_right {G : Type w} [] [] (a : G) :
IsOpenMap fun x => x - a
theorem isOpenMap_div_right {G : Type w} [] [] [] (a : G) :
IsOpenMap fun x => x / a
theorem isClosedMap_sub_right {G : Type w} [] [] (a : G) :
IsClosedMap fun x => x - a
theorem isClosedMap_div_right {G : Type w} [] [] [] (a : G) :
IsClosedMap fun x => x / a
theorem tendsto_sub_nhds_zero_iff {G : Type w} [] [] {α : Type u_1} {l : } {x : G} {u : αG} :
Filter.Tendsto (fun n => u n - x) l (nhds 0) Filter.Tendsto u l (nhds x)
theorem tendsto_div_nhds_one_iff {G : Type w} [] [] [] {α : Type u_1} {l : } {x : G} {u : αG} :
Filter.Tendsto (fun n => u n / x) l (nhds 1) Filter.Tendsto u l (nhds x)
theorem nhds_translation_sub {G : Type w} [] [] (x : G) :
Filter.comap (fun x => x - x) (nhds 0) = nhds x
theorem nhds_translation_div {G : Type w} [] [] [] (x : G) :
Filter.comap (fun x => x / x) (nhds 1) = 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 IsOpen.vadd_left {α : Type u} {β : Type v} [] [] [] [] {s : Set α} {t : Set β} (ht : ) :
IsOpen (s +ᵥ t)
theorem IsOpen.smul_left {α : Type u} {β : Type v} [] [] [] [] {s : Set α} {t : Set β} (ht : ) :
IsOpen (s t)
theorem subset_interior_vadd_right {α : Type u} {β : Type v} [] [] [] [] {s : Set α} {t : Set β} :
theorem subset_interior_smul_right {α : Type u} {β : Type v} [] [] [] [] {s : Set α} {t : Set β} :
theorem vadd_mem_nhds {α : Type u} {β : Type v} [] [] [] [] {t : Set β} (a : α) {x : β} (ht : t nhds x) :
a +ᵥ t nhds (a +ᵥ x)
theorem smul_mem_nhds {α : Type u} {β : Type v} [] [] [] [] {t : Set β} (a : α) {x : β} (ht : t nhds x) :
a t nhds (a x)
theorem subset_interior_vadd {α : Type u} {β : Type v} [] [] [] [] {s : Set α} {t : Set β} [] :
theorem subset_interior_smul {α : Type u} {β : Type v} [] [] [] [] {s : Set α} {t : Set β} [] :
abbrev IsClosed.vadd_left_of_isCompact.match_1 {α : Type u_2} {β : Type u_1} [] [] {s : Set α} {t : Set β} (x : β) (motive : x s +ᵥ tProp) :
(h : x s +ᵥ t) → ((g : α) → (y : β) → (hgs : g s) → (hyt : y t) → (hgyx : (fun x x_1 => x +ᵥ x_1) g y = x) → motive (_ : a b, a s b t (fun x x_1 => x +ᵥ x_1) a b = x)) → motive h
Instances For
theorem IsClosed.vadd_left_of_isCompact {α : Type u} {β : Type v} [] [] [] [] [] [] {s : Set α} {t : Set β} (ht : ) (hs : ) :
theorem IsClosed.smul_left_of_isCompact {α : Type u} {β : Type v} [] [] [] [] [] [] {s : Set α} {t : Set β} (ht : ) (hs : ) :

One may expect a version of IsClosed.smul_left_of_isCompact where t is compact and s is closed, but such a lemma can't be true in this level of generality. For a counterexample, consider ℚ acting on ℝ by translation, and let s : set ℚ := univ, t : set ℝ := {0}. Then s is closed and t is compact, but s +ᵥ t is the set of all rationals, which is definitely not closed in ℝ. To fix the proof, we would need to make two additional assumptions:

• for any x ∈ t, s • {x} is closed
• for any x ∈ t, there is a continuous function g : s • {x} → s such that, for all y ∈ s • {x}, we have y = (g y) • x These are fairly specific hypotheses so we don't state this version of the lemmas, but an interesting fact is that these two assumptions are verified in the case of a NormedAddTorsor (or really, any AddTorsor with continuous -ᵥ). We prove this special case in IsClosed.vadd_right_of_isCompact.
theorem AddAction.isClosedMap_quotient {α : Type u} {β : Type v} [] [] [] [] [] [] [] :
IsClosedMap Quotient.mk'
theorem MulAction.isClosedMap_quotient {α : Type u} {β : Type v} [] [] [] [] [] [] [] :
IsClosedMap Quotient.mk'
theorem IsOpen.add_left {α : Type u} [] [] [] {s : Set α} {t : Set α} :
IsOpen (s + t)
theorem IsOpen.mul_left {α : Type u} [] [] [] {s : Set α} {t : Set α} :
IsOpen (s * t)
theorem subset_interior_add_right {α : Type u} [] [] [] {s : Set α} {t : Set α} :
s + interior (s + t)
theorem subset_interior_mul_right {α : Type u} [] [] [] {s : Set α} {t : Set α} :
s * interior (s * t)
theorem subset_interior_add {α : Type u} [] [] [] {s : Set α} {t : Set α} :
interior (s + t)
theorem subset_interior_mul {α : Type u} [] [] [] {s : Set α} {t : Set α} :
interior (s * t)
theorem singleton_add_mem_nhds {α : Type u} [] [] [] {s : Set α} (a : α) {b : α} (h : s nhds b) :
{a} + s nhds (a + b)
theorem singleton_mul_mem_nhds {α : Type u} [] [] [] {s : Set α} (a : α) {b : α} (h : s nhds b) :
{a} * s nhds (a * b)
theorem singleton_add_mem_nhds_of_nhds_zero {α : Type u} [] [] [] {s : Set α} (a : α) (h : s nhds 0) :
{a} + s nhds a
theorem singleton_mul_mem_nhds_of_nhds_one {α : Type u} [] [] [] {s : Set α} (a : α) (h : s nhds 1) :
{a} * s nhds a
theorem IsOpen.add_right {α : Type u} [] [] [] {s : Set α} {t : Set α} (hs : ) :
IsOpen (s + t)
theorem IsOpen.mul_right {α : Type u} [] [] [] {s : Set α} {t : Set α} (hs : ) :
IsOpen (s * t)
theorem subset_interior_add_left {α : Type u} [] [] [] {s : Set α} {t : Set α} :
+ t interior (s + t)
theorem subset_interior_mul_left {α : Type u} [] [] [] {s : Set α} {t : Set α} :
* t interior (s * t)
theorem subset_interior_add' {α : Type u} [] [] [] {s : Set α} {t : Set α} :
interior (s + t)
theorem subset_interior_mul' {α : Type u} [] [] [] {s : Set α} {t : Set α} :
interior (s * t)
theorem add_singleton_mem_nhds {α : Type u} [] [] [] {s : Set α} (a : α) {b : α} (h : s nhds b) :
s + {a} nhds (b + a)
theorem mul_singleton_mem_nhds {α : Type u} [] [] [] {s : Set α} (a : α) {b : α} (h : s nhds b) :
s * {a} nhds (b * a)
theorem add_singleton_mem_nhds_of_nhds_zero {α : Type u} [] [] [] {s : Set α} (a : α) (h : s nhds 0) :
s + {a} nhds a
theorem mul_singleton_mem_nhds_of_nhds_one {α : Type u} [] [] [] {s : Set α} (a : α) (h : s nhds 1) :
s * {a} nhds a
theorem IsOpen.sub_left {α : Type u} [] [] {s : Set α} {t : Set α} (ht : ) :
IsOpen (s - t)
theorem IsOpen.div_left {α : Type u} [] [] [] {s : Set α} {t : Set α} (ht : ) :
IsOpen (s / t)
theorem IsOpen.sub_right {α : Type u} [] [] {s : Set α} {t : Set α} (hs : ) :
IsOpen (s - t)
theorem IsOpen.div_right {α : Type u} [] [] [] {s : Set α} {t : Set α} (hs : ) :
IsOpen (s / t)
theorem subset_interior_sub_left {α : Type u} [] [] {s : Set α} {t : Set α} :
- t interior (s - t)
theorem subset_interior_div_left {α : Type u} [] [] [] {s : Set α} {t : Set α} :
/ t interior (s / t)
theorem subset_interior_sub_right {α : Type u} [] [] {s : Set α} {t : Set α} :
s - interior (s - t)
theorem subset_interior_div_right {α : Type u} [] [] [] {s : Set α} {t : Set α} :
s / interior (s / t)
theorem subset_interior_sub {α : Type u} [] [] {s : Set α} {t : Set α} :
interior (s - t)
theorem subset_interior_div {α : Type u} [] [] [] {s : Set α} {t : Set α} :
interior (s / t)
theorem IsOpen.add_closure {α : Type u} [] [] {s : Set α} (hs : ) (t : Set α) :
s + = s + t
theorem IsOpen.mul_closure {α : Type u} [] [] [] {s : Set α} (hs : ) (t : Set α) :
s * = s * t
theorem IsOpen.closure_add {α : Type u} [] [] {t : Set α} (ht : ) (s : Set α) :
+ t = s + t
theorem IsOpen.closure_mul {α : Type u} [] [] [] {t : Set α} (ht : ) (s : Set α) :
* t = s * t
theorem IsOpen.sub_closure {α : Type u} [] [] {s : Set α} (hs : ) (t : Set α) :
s - = s - t
theorem IsOpen.div_closure {α : Type u} [] [] [] {s : Set α} (hs : ) (t : Set α) :
s / = s / t
theorem IsOpen.closure_sub {α : Type u} [] [] {t : Set α} (ht : ) (s : Set α) :
- t = s - t
theorem IsOpen.closure_div {α : Type u} [] [] [] {t : Set α} (ht : ) (s : Set α) :
/ t = s / t
theorem IsClosed.add_left_of_isCompact {α : Type u} [] [] {s : Set α} {t : Set α} (ht : ) (hs : ) :
IsClosed (s + t)
theorem IsClosed.mul_left_of_isCompact {α : Type u} [] [] [] {s : Set α} {t : Set α} (ht : ) (hs : ) :
IsClosed (s * t)
theorem IsClosed.add_right_of_isCompact {α : Type u} [] [] {s : Set α} {t : Set α} (ht : ) (hs : ) :
IsClosed (t + s)
theorem IsClosed.mul_right_of_isCompact {α : Type u} [] [] [] {s : Set α} {t : Set α} (ht : ) (hs : ) :
IsClosed (t * s)
theorem QuotientAddGroup.isClosedMap_coe {α : Type u} [] [] {H : } (hH : ) :
theorem QuotientGroup.isClosedMap_coe {α : Type u} [] [] [] {H : } (hH : ) :
IsClosedMap QuotientGroup.mk
theorem TopologicalAddGroup.t1Space (G : Type w) [] [] [] (h : IsClosed {0}) :
theorem TopologicalGroup.t1Space (G : Type w) [] [] [] (h : IsClosed {1}) :
instance TopologicalGroup.regularSpace (G : Type w) [] [] [] :
theorem TopologicalAddGroup.t2Space_of_zero_sep {G : Type w} [] [] (H : ∀ (x : G), x 0U, U nhds 0 ¬x U) :
theorem TopologicalGroup.t2Space_of_one_sep {G : Type w} [] [] [] (H : ∀ (x : G), x 1U, U nhds 1 ¬x U) :
instance AddSubgroup.t3_quotient_of_isClosed {G : Type w} [] [] (S : ) [hS : IsClosed S] :
T3Space (G S)
theorem AddSubgroup.t3_quotient_of_isClosed.proof_1 {G : Type u_1} [] [] (S : ) [hS : IsClosed S] :
T3Space (G S)
instance Subgroup.t3_quotient_of_isClosed {G : Type w} [] [] [] (S : ) [] [hS : IsClosed S] :
T3Space (G S)
theorem AddSubgroup.properlyDiscontinuousVAdd_of_tendsto_cofinite {G : Type w} [] [] (S : ) (hS : Filter.Tendsto (↑()) Filter.cofinite ()) :

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 DiscreteTopology.

theorem Subgroup.properlyDiscontinuousSMul_of_tendsto_cofinite {G : Type w} [] [] [] (S : ) (hS : Filter.Tendsto (↑()) Filter.cofinite ()) :

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 DiscreteTopology.)

theorem AddSubgroup.properlyDiscontinuousVAdd_opposite_of_tendsto_cofinite {G : Type w} [] [] (S : ) (hS : Filter.Tendsto (↑()) Filter.cofinite ()) :

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 DiscreteTopology.)

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

theorem Subgroup.properlyDiscontinuousSMul_opposite_of_tendsto_cofinite {G : Type w} [] [] [] (S : ) (hS : Filter.Tendsto (↑()) Filter.cofinite ()) :
ProperlyDiscontinuousSMul { x // x Subgroup.opposite S } G

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 DiscreteTopology.)

If G is Hausdorff, this can be combined with t2Space_of_properlyDiscontinuousSMul_of_t2Space 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 : Set G} {U : Set G} (hK : ) (hU : ) (hKU : K U) :
V, V nhds 0 K + V U

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

theorem compact_open_separated_mul_right {G : Type w} [] [] [] {K : Set G} {U : Set G} (hK : ) (hU : ) (hKU : K U) :
V, V nhds 1 K * V U

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

theorem compact_open_separated_add_left {G : Type w} [] [] [] {K : Set G} {U : Set G} (hK : ) (hU : ) (hKU : K U) :
V, V nhds 0 V + K U

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

theorem compact_open_separated_mul_left {G : Type w} [] [] [] {K : Set G} {U : Set G} (hK : ) (hU : ) (hKU : K U) :
V, V nhds 1 V * K U

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

theorem compact_covered_by_add_left_translates {G : Type w} [] [] {K : Set G} {V : Set G} (hK : ) (hV : ) :
t, K ⋃ (g : G) (_ : g t), (fun h => 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} [] [] [] {K : Set G} {V : Set G} (hK : ) (hV : ) :
t, K ⋃ (g : G) (_ : g t), (fun h => g * h) ⁻¹' V

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

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

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

theorem exists_disjoint_vadd_of_isCompact {G : Type w} [] [] [] {K : Set G} {L : Set G} (hK : ) (hL : ) :
g, Disjoint K (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_isCompact {G : Type w} [] [] [] [] {K : Set G} {L : Set G} (hK : ) (hL : ) :
g, Disjoint K (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 exists_isCompact_isClosed_subset_isCompact_nhds_zero {G : Type w} [] [] {L : Set G} (Lcomp : ) (L1 : L nhds 0) :
K, K L K nhds 0

A compact neighborhood of 0 in a topological additive group admits a closed compact subset that is a neighborhood of 0.

theorem exists_isCompact_isClosed_subset_isCompact_nhds_one {G : Type w} [] [] [] {L : Set G} (Lcomp : ) (L1 : L nhds 1) :
K, K L K nhds 1

A compact neighborhood of 1 in a topological group admits a closed compact subset that is a neighborhood of 1.

theorem local_isCompact_isClosed_nhds_of_addGroup {G : Type w} [] [] {U : Set G} (hU : U nhds 0) :
K, 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_isCompact_isClosed_nhds_of_group {G : Type w} [] [] [] {U : Set G} (hU : U nhds 1) :
K, 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.

abbrev exists_isCompact_isClosed_nhds_zero.match_2 (G : Type u_1) [] [] (motive : (s, s nhds 0) → Prop) :
(x : s, s nhds 0) → ((_L : Set G) → (Lcomp : ) → (L1 : _L nhds 0) → motive (_ : s, s nhds 0)) → motive x
Instances For