# 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 : G) => (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.

Equations
• = let __src := ; { toEquiv := __src, continuous_toFun := , continuous_invFun := }
Instances For
theorem Homeomorph.addLeft.proof_2 {G : Type u_1} [] [] [] (a : G) :
Continuous fun (x : G) => (-toAddUnits a) + x
def Homeomorph.mulLeft {G : Type w} [] [] [] (a : G) :
G ≃ₜ G

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

Equations
• = let __src := ; { toEquiv := __src, continuous_toFun := , continuous_invFun := }
Instances For
@[simp]
theorem Homeomorph.coe_addLeft {G : Type w} [] [] [] (a : G) :
= fun (x : G) => a + x
@[simp]
theorem Homeomorph.coe_mulLeft {G : Type w} [] [] [] (a : G) :
= fun (x : G) => a * x
theorem Homeomorph.addLeft_symm {G : Type w} [] [] [] (a : G) :
.symm =
theorem Homeomorph.mulLeft_symm {G : Type w} [] [] [] (a : G) :
.symm =
theorem isOpenMap_add_left {G : Type w} [] [] [] (a : G) :
IsOpenMap fun (x : G) => a + x
theorem isOpenMap_mul_left {G : Type w} [] [] [] (a : G) :
IsOpenMap fun (x : G) => a * x
theorem IsOpen.left_addCoset {G : Type w} [] [] [] {U : Set G} (h : ) (x : G) :
IsOpen (x +ᵥ U)
theorem IsOpen.leftCoset {G : Type w} [] [] [] {U : Set G} (h : ) (x : G) :
IsOpen (x U)
theorem isClosedMap_add_left {G : Type w} [] [] [] (a : G) :
IsClosedMap fun (x : G) => a + x
theorem isClosedMap_mul_left {G : Type w} [] [] [] (a : G) :
IsClosedMap fun (x : G) => 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 : G) => id x + (-toAddUnits a)
theorem Homeomorph.addRight.proof_1 {G : Type u_1} [] [] [] (a : G) :
Continuous fun (x : G) => 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.

Equations
• = let __src := ; { toEquiv := __src, continuous_toFun := , continuous_invFun := }
Instances For
def Homeomorph.mulRight {G : Type w} [] [] [] (a : G) :
G ≃ₜ G

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

Equations
• = let __src := ; { toEquiv := __src, continuous_toFun := , continuous_invFun := }
Instances For
@[simp]
theorem Homeomorph.coe_addRight {G : Type w} [] [] [] (a : G) :
= fun (x : G) => x + a
@[simp]
theorem Homeomorph.coe_mulRight {G : Type w} [] [] [] (a : G) :
= fun (x : G) => x * a
theorem Homeomorph.addRight_symm {G : Type w} [] [] [] (a : G) :
.symm =
theorem Homeomorph.mulRight_symm {G : Type w} [] [] [] (a : G) :
.symm =
theorem isOpenMap_add_right {G : Type w} [] [] [] (a : G) :
IsOpenMap fun (x : G) => x + a
theorem isOpenMap_mul_right {G : Type w} [] [] [] (a : G) :
IsOpenMap fun (x : G) => 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) :
IsOpen ( U)
theorem isClosedMap_add_right {G : Type w} [] [] [] (a : G) :
IsClosedMap fun (x : G) => x + a
theorem isClosedMap_mul_right {G : Type w} [] [] [] (a : G) :
IsClosedMap fun (x : G) => 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_isOpen_singleton_zero {G : Type w} [] [] [] (h : IsOpen {0}) :
theorem discreteTopology_of_isOpen_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
theorem ContinuousNeg.continuous_neg {G : Type u} [] [Neg G] [self : ] :
Continuous fun (a : G) => -a
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 ContinuousInv.continuous_inv {G : Type u} [] [Inv G] [self : ] :
Continuous fun (a : G) => a⁻¹
theorem ContinuousNeg.induced {α : Type u_1} {β : Type u_2} {F : Type u_3} [FunLike F α β] [] [] [] [tβ : ] [] (f : F) :
theorem ContinuousInv.induced {α : Type u_1} {β : Type u_2} {F : Type u_3} [FunLike F α β] [] [] [] [tβ : ] [] (f : F) :
theorem Specializes.neg {G : Type w} [] [Neg G] [] {x : G} {y : G} (h : x y) :
(-x) (-y)
theorem Specializes.inv {G : Type w} [] [Inv G] [] {x : G} {y : G} (h : x y) :
theorem Inseparable.neg {G : Type w} [] [Neg G] [] {x : G} {y : G} (h : ) :
theorem Inseparable.inv {G : Type w} [] [Inv G] [] {x : G} {y : G} (h : ) :
theorem Specializes.zsmul {G : Type u_1} [] [] [] [] {x : G} {y : G} (h : x y) (m : ) :
(m x) (m y)
@[inline]
abbrev Specializes.zsmul.match_1 (motive : ) :
∀ (x : ), (∀ (n : ), motive (Int.ofNat n))(∀ (n : ), motive (Int.negSucc n))motive x
Equations
• =
Instances For
theorem Specializes.zpow {G : Type u_1} [] [] [] [] {x : G} {y : G} (h : x y) (m : ) :
(x ^ m) (y ^ m)
theorem Inseparable.zsmul {G : Type u_1} [] [] [] [] {x : G} {y : G} (h : ) (m : ) :
Inseparable (m x) (m y)
theorem Inseparable.zpow {G : Type u_1} [] [] [] [] {x : G} {y : G} (h : ) (m : ) :
Inseparable (x ^ m) (y ^ m)
instance instContinuousNegULift {G : Type w} [] [Neg G] [] :
Equations
• =
instance instContinuousInvULift {G : Type w} [] [Inv G] [] :
Equations
• =
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) (nhds a⁻¹)
theorem Filter.Tendsto.neg {G : Type w} {α : Type u} [] [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 {G : Type w} {α : Type u} [] [Inv 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 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 {G : Type w} {α : Type u} [] [Neg G] [] [] {f : αG} (hf : ) :
Continuous fun (x : α) => -f x
theorem Continuous.inv {G : Type w} {α : Type u} [] [Inv G] [] [] {f : αG} (hf : ) :
Continuous fun (x : α) => (f x)⁻¹
theorem ContinuousAt.neg {G : Type w} {α : Type u} [] [Neg G] [] [] {f : αG} {x : α} (hf : ) :
ContinuousAt (fun (x : α) => -f x) x
theorem ContinuousAt.inv {G : Type w} {α : Type u} [] [Inv G] [] [] {f : αG} {x : α} (hf : ) :
ContinuousAt (fun (x : α) => (f x)⁻¹) x
theorem ContinuousOn.neg {G : Type w} {α : Type u} [] [Neg G] [] [] {f : αG} {s : Set α} (hf : ) :
ContinuousOn (fun (x : α) => -f x) s
theorem ContinuousOn.inv {G : Type w} {α : Type u} [] [Inv G] [] [] {f : αG} {s : Set α} (hf : ) :
ContinuousOn (fun (x : α) => (f x)⁻¹) s
theorem ContinuousWithinAt.neg {G : Type w} {α : Type u} [] [Neg G] [] [] {f : αG} {s : Set α} {x : α} (hf : ) :
ContinuousWithinAt (fun (x : α) => -f x) s x
theorem ContinuousWithinAt.inv {G : Type w} {α : Type u} [] [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] [] :
Equations
• =
instance Prod.continuousInv {G : Type w} {H : Type x} [] [Inv G] [] [] [Inv H] [] :
Equations
• =
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)
Equations
• =
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)
Equations
• =
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.

Equations
• =
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.

Equations
• =
@[instance 100]
instance continuousNeg_of_discreteTopology {H : Type x} [] [Neg H] [] :
Equations
• =
@[instance 100]
instance continuousInv_of_discreteTopology {H : Type x} [] [Inv H] [] :
Equations
• =
theorem isClosed_setOf_map_neg (G₁ : Type u_2) (G₂ : Type u_3) [] [T2Space G₂] [Neg G₁] [Neg G₂] [] :
IsClosed {f : G₁G₂ | ∀ (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 : G₁G₂ | ∀ (x : G₁), f x⁻¹ = (f x)⁻¹}
Equations
• =
Equations
• =
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.

Equations
• = let __src := ; { toEquiv := __src, continuous_toFun := , continuous_invFun := }
Instances For
theorem Homeomorph.neg.proof_1 (G : Type u_1) [] [] [] :
Continuous fun (a : G) => -a
def Homeomorph.inv (G : Type u_1) [] [] [] :
G ≃ₜ G

Inversion in a topological group as a homeomorphism.

Equations
• = let __src := ; { toEquiv := __src, continuous_toFun := , continuous_invFun := }
Instances For
@[simp]
theorem Homeomorph.coe_neg {G : Type u_1} [] [] [] :
= Neg.neg
@[simp]
theorem Homeomorph.coe_inv {G : Type u_1} [] [] [] :
= Inv.inv
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) :
@[simp]
theorem continuous_neg_iff {G : Type w} {α : Type u} [] [] [] [] {f : αG} :
@[simp]
theorem continuous_inv_iff {G : Type w} {α : Type u} [] [] [] [] {f : αG} :
@[simp]
theorem continuousAt_neg_iff {G : Type w} {α : Type u} [] [] [] [] {f : αG} {x : α} :
@[simp]
theorem continuousAt_inv_iff {G : Type w} {α : Type u} [] [] [] [] {f : αG} {x : α} :
@[simp]
theorem continuousOn_neg_iff {G : Type w} {α : Type u} [] [] [] [] {f : αG} {s : Set α} :
@[simp]
theorem continuousOn_inv_iff {G : Type w} {α : Type u} [] [] [] [] {f : αG} {s : Set α} :
theorem Continuous.of_inv {G : Type w} {α : Type u} [] [] [] [] {f : αG} :

Alias of the forward direction of continuous_inv_iff.

theorem Continuous.of_neg {G : Type w} {α : Type u} [] [] [] [] {f : αG} :
Continuous (-f)
theorem ContinuousAt.of_inv {G : Type w} {α : Type u} [] [] [] [] {f : αG} {x : α} :

Alias of the forward direction of continuousAt_inv_iff.

theorem ContinuousAt.of_neg {G : Type w} {α : Type u} [] [] [] [] {f : αG} {x : α} :
ContinuousAt (-f) x
theorem ContinuousOn.of_inv {G : Type w} {α : Type u} [] [] [] [] {f : αG} {s : Set α} :

Alias of the forward direction of continuousOn_inv_iff.

theorem ContinuousOn.of_neg {G : Type w} {α : Type u} [] [] [] [] {f : αG} {s : Set α} :
ContinuousOn (-f) s
theorem continuousNeg_sInf {G : Type w} [Neg G] {ts : } (h : tts, ) :
theorem continuousInv_sInf {G : Type w} [Inv G] {ts : } (h : tts, ) :
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} [] [] [] :
Equations
• =
theorem TopologicalAddGroup.continuous_conj_sum {G : Type w} [] [Neg G] [Add G] [] [] :
Continuous fun (g : G × G) => g.1 + g.2 + -g.1

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 × G) => g.1 * g.2 * g.1⁻¹

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) => 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) => 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) => 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) => g * h * g⁻¹

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

instance instTopologicalGroupULift {G : Type w} [] [] [] :
Equations
• =
theorem continuous_zsmul {G : Type w} [] [] (z : ) :
Continuous fun (a : G) => z a
theorem continuous_zpow {G : Type w} [] [] [] (z : ) :
Continuous fun (a : G) => a ^ z
instance AddGroup.continuousConstSMul_int {A : Type u_1} [] [] :
Equations
• =
instance AddGroup.continuousSMul_int {A : Type u_1} [] [] :
Equations
• =
theorem Continuous.zsmul {G : Type w} {α : Type u} [] [] [] {f : αG} (h : ) (z : ) :
Continuous fun (b : α) => z f b
theorem Continuous.zpow {G : Type w} {α : Type u} [] [] [] [] {f : αG} (h : ) (z : ) :
Continuous fun (b : α) => f b ^ z
theorem continuousOn_zsmul {G : Type w} [] [] {s : Set G} (z : ) :
ContinuousOn (fun (x : G) => z x) s
theorem continuousOn_zpow {G : Type w} [] [] [] {s : Set G} (z : ) :
ContinuousOn (fun (x : G) => x ^ z) s
theorem continuousAt_zsmul {G : Type w} [] [] (x : G) (z : ) :
ContinuousAt (fun (x : G) => z x) x
theorem continuousAt_zpow {G : Type w} [] [] [] (x : G) (z : ) :
ContinuousAt (fun (x : G) => 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 {G : Type w} {α : Type u} [] [] [] {f : αG} {x : α} {s : Set α} (hf : ) (z : ) :
ContinuousWithinAt (fun (x : α) => z f x) s x
theorem ContinuousWithinAt.zpow {G : Type w} {α : Type u} [] [] [] [] {f : αG} {x : α} {s : Set α} (hf : ) (z : ) :
ContinuousWithinAt (fun (x : α) => f x ^ z) s x
theorem ContinuousAt.zsmul {G : Type w} {α : Type u} [] [] [] {f : αG} {x : α} (hf : ) (z : ) :
ContinuousAt (fun (x : α) => z f x) x
theorem ContinuousAt.zpow {G : Type w} {α : Type u} [] [] [] [] {f : αG} {x : α} (hf : ) (z : ) :
ContinuousAt (fun (x : α) => f x ^ z) x
theorem ContinuousOn.zsmul {G : Type w} {α : Type u} [] [] [] {f : αG} {s : Set α} (hf : ) (z : ) :
ContinuousOn (fun (x : α) => z f x) s
theorem ContinuousOn.zpow {G : Type w} {α : Type u} [] [] [] [] {f : αG} {s : Set α} (hf : ) (z : ) :
ContinuousOn (fun (x : α) => f x ^ z) s
theorem tendsto_neg_nhdsWithin_Ioi {H : Type x} [] [] {a : H} :
theorem tendsto_inv_nhdsWithin_Ioi {H : Type x} [] [] [] {a : H} :
theorem tendsto_neg_nhdsWithin_Iio {H : Type x} [] [] {a : H} :
theorem tendsto_inv_nhdsWithin_Iio {H : Type x} [] [] [] {a : H} :
theorem tendsto_neg_nhdsWithin_Ioi_neg {H : Type x} [] [] {a : H} :
theorem tendsto_neg_nhdsWithin_Iio_neg {H : Type x} [] [] {a : H} :
theorem tendsto_neg_nhdsWithin_Ici {H : Type x} [] [] {a : H} :
theorem tendsto_inv_nhdsWithin_Ici {H : Type x} [] [] [] {a : H} :
theorem tendsto_neg_nhdsWithin_Iic {H : Type x} [] [] {a : H} :
theorem tendsto_inv_nhdsWithin_Iic {H : Type x} [] [] [] {a : H} :
theorem tendsto_neg_nhdsWithin_Ici_neg {H : Type x} [] [] {a : H} :
theorem tendsto_neg_nhdsWithin_Iic_neg {H : Type x} [] [] {a : H} :
instance instTopologicalAddGroupSum {G : Type w} {H : Type x} [] [] [] [] :
Equations
• =
instance instTopologicalGroupProd {G : Type w} {H : Type x} [] [] [] [] [] [] :
Equations
• =
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)
Equations
• =
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)
Equations
• =
instance instContinuousNegAddOpposite {α : Type u} [] [Neg α] [] :
Equations
• =
instance instContinuousInvMulOpposite {α : Type u} [] [Inv α] [] :
Equations
• =

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

Equations
• =
instance instTopologicalGroupMulOpposite {α : Type u} [] [] [] :

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

Equations
• =
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) :
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.

Equations
• = let __src := (Equiv.refl G).prodShear Equiv.addLeft; { toEquiv := __src, continuous_toFun := , continuous_invFun := }
Instances For
theorem Homeomorph.shearAddRight.proof_2 (G : Type u_1) [] [] :
Continuous fun (x : G × G) => (x.1, (Equiv.symm (Equiv.addLeft ((Equiv.refl G).symm x.1))) x.2)
theorem Homeomorph.shearAddRight.proof_1 (G : Type u_1) [] [] :
Continuous fun (x : G × G) => (x.1, (Equiv.addLeft x.1) x.2)
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.

Equations
• = let __src := (Equiv.refl G).prodShear Equiv.mulLeft; { toEquiv := __src, continuous_toFun := , continuous_invFun := }
Instances For
@[simp]
theorem Homeomorph.shearAddRight_coe (G : Type w) [] [] :
= fun (z : G × G) => (z.1, z.1 + z.2)
@[simp]
theorem Homeomorph.shearMulRight_coe (G : Type w) [] [] [] :
= fun (z : G × G) => (z.1, z.1 * z.2)
@[simp]
theorem Homeomorph.shearAddRight_symm_coe (G : Type w) [] [] :
.symm = fun (z : G × G) => (z.1, -z.1 + z.2)
@[simp]
theorem Homeomorph.shearMulRight_symm_coe (G : Type w) [] [] [] :
.symm = fun (z : G × G) => (z.1, z.1⁻¹ * z.2)
theorem Inducing.topologicalAddGroup {G : Type w} {H : Type x} [] [] {F : Type u_1} [] [] [FunLike F H G] [] (f : F) (hf : Inducing f) :
theorem Inducing.topologicalGroup {G : Type w} {H : Type x} [] [] [] {F : Type u_1} [] [] [FunLike F H G] [] (f : F) (hf : Inducing f) :
theorem topologicalAddGroup_induced {G : Type w} {H : Type x} [] [] {F : Type u_1} [] [FunLike F H G] [] (f : F) :
theorem topologicalGroup_induced {G : Type w} {H : Type x} [] [] [] {F : Type u_1} [] [FunLike F H G] [] (f : F) :
instance AddSubgroup.instTopologicalAddGroupSubtypeMem {G : Type w} [] [] (S : ) :
Equations
• =
instance Subgroup.instTopologicalGroupSubtypeMem {G : Type w} [] [] [] (S : ) :
Equations
• =
theorem AddSubgroup.topologicalClosure.proof_2 {G : Type u_1} [] [] (s : ) :
0 s.topologicalClosure.carrier
theorem AddSubgroup.topologicalClosure.proof_3 {G : Type u_1} [] [] (s : ) {g : G} (hg : g { carrier := closure s, add_mem' := , zero_mem' := }.carrier) :
-g { carrier := closure s, add_mem' := , zero_mem' := }.carrier
def AddSubgroup.topologicalClosure {G : Type w} [] [] (s : ) :

The (topological-space) closure of an additive subgroup of an additive topological group is itself an additive subgroup.

Equations
• s.topologicalClosure = let __src := s.topologicalClosure; { carrier := closure s, add_mem' := , zero_mem' := , neg_mem' := }
Instances For
theorem AddSubgroup.topologicalClosure.proof_1 {G : Type u_1} [] [] (s : ) :
∀ {a b : G}, a s.topologicalClosure.carrierb s.topologicalClosure.carriera + b s.topologicalClosure.carrier
def Subgroup.topologicalClosure {G : Type w} [] [] [] (s : ) :

The (topological-space) closure of a subgroup of a topological group is itself a subgroup.

Equations
• s.topologicalClosure = let __src := s.topologicalClosure; { carrier := closure s, mul_mem' := , one_mem' := , inv_mem' := }
Instances For
@[simp]
theorem AddSubgroup.topologicalClosure_coe {G : Type w} [] [] {s : } :
s.topologicalClosure = closure s
@[simp]
theorem Subgroup.topologicalClosure_coe {G : Type w} [] [] [] {s : } :
s.topologicalClosure = closure s
theorem AddSubgroup.le_topologicalClosure {G : Type w} [] [] (s : ) :
s s.topologicalClosure
theorem Subgroup.le_topologicalClosure {G : Type w} [] [] [] (s : ) :
s s.topologicalClosure
theorem AddSubgroup.isClosed_topologicalClosure {G : Type w} [] [] (s : ) :
IsClosed s.topologicalClosure
theorem Subgroup.isClosed_topologicalClosure {G : Type w} [] [] [] (s : ) :
IsClosed s.topologicalClosure
theorem AddSubgroup.topologicalClosure_minimal {G : Type w} [] [] (s : ) {t : } (h : s t) (ht : IsClosed t) :
s.topologicalClosure t
theorem Subgroup.topologicalClosure_minimal {G : Type w} [] [] [] (s : ) {t : } (h : s t) (ht : IsClosed t) :
s.topologicalClosure t
theorem DenseRange.topologicalClosure_map_addSubgroup {G : Type w} {H : Type x} [] [] [] [] {f : G →+ H} (hf : ) (hf' : ) {s : } (hs : s.topologicalClosure = ) :
theorem DenseRange.topologicalClosure_map_subgroup {G : Type w} {H : Type x} [] [] [] [] [] [] {f : G →* H} (hf : ) (hf' : ) {s : } (hs : s.topologicalClosure = ) :
(Subgroup.map f s).topologicalClosure =
theorem AddSubgroup.is_normal_topologicalClosure {G : Type u_1} [] [] (N : ) [N.Normal] :
N.topologicalClosure.Normal

The topological closure of a normal additive subgroup is normal.

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

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.

Equations
• = { carrier := , add_mem' := , zero_mem' := , neg_mem' := }
Instances For
def Subgroup.connectedComponentOfOne (G : Type u_1) [] [] [] :

The connected component of 1 is a subgroup of G.

Equations
• = { carrier := , mul_mem' := , one_mem' := , inv_mem' := }
Instances For
def AddSubgroup.addCommGroupTopologicalClosure {G : Type w} [] [] [] (s : ) (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
Instances For
theorem AddSubgroup.addCommGroupTopologicalClosure.proof_1 {G : Type u_1} [] [] [] (s : ) (hs : ∀ (x y : s), x + y = y + x) (a : s.topologicalClosure) (b : s.topologicalClosure) :
a + b = b + a
def Subgroup.commGroupTopologicalClosure {G : Type w} [] [] [] [] (s : ) (hs : ∀ (x y : s), x * y = y * x) :
CommGroup s.topologicalClosure

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

Equations
• s.commGroupTopologicalClosure hs = let __src := s.topologicalClosure.toGroup; let __src_1 := s.commMonoidTopologicalClosure hs;
Instances For
theorem AddSubgroup.coe_topologicalClosure_bot (G : Type w) [] [] :
.topologicalClosure = closure {0}
theorem Subgroup.coe_topologicalClosure_bot (G : Type w) [] [] [] :
.topologicalClosure = closure {1}
theorem exists_nhds_half_neg {G : Type w} [] [] {s : Set G} (hs : s nhds 0) :
Vnhds 0, vV, wV, v - w s
theorem exists_nhds_split_inv {G : Type w} [] [] [] {s : Set G} (hs : s nhds 1) :
Vnhds 1, vV, wV, v / w s
theorem nhds_translation_add_neg {G : Type w} [] [] (x : G) :
Filter.comap (fun (x_1 : G) => x_1 + -x) (nhds 0) = nhds x
theorem nhds_translation_mul_inv {G : Type w} [] [] [] (x : G) :
Filter.comap (fun (x_1 : G) => x_1 * x⁻¹) (nhds 1) = nhds x
@[simp]
theorem map_add_left_nhds {G : Type w} [] [] (x : G) (y : G) :
Filter.map (fun (x_1 : G) => x + x_1) (nhds y) = nhds (x + y)
@[simp]
theorem map_mul_left_nhds {G : Type w} [] [] [] (x : G) (y : G) :
Filter.map (fun (x_1 : G) => x * x_1) (nhds y) = nhds (x * y)
theorem map_add_left_nhds_zero {G : Type w} [] [] (x : G) :
Filter.map (fun (x_1 : G) => x + x_1) (nhds 0) = nhds x
theorem map_mul_left_nhds_one {G : Type w} [] [] [] (x : G) :
Filter.map (fun (x_1 : G) => x * x_1) (nhds 1) = nhds x
@[simp]
theorem map_add_right_nhds {G : Type w} [] [] (x : G) (y : G) :
Filter.map (fun (x_1 : G) => x_1 + x) (nhds y) = nhds (y + x)
@[simp]
theorem map_mul_right_nhds {G : Type w} [] [] [] (x : G) (y : G) :
Filter.map (fun (x_1 : G) => x_1 * x) (nhds y) = nhds (y * x)
theorem map_add_right_nhds_zero {G : Type w} [] [] (x : G) :
Filter.map (fun (x_1 : G) => x_1 + x) (nhds 0) = nhds x
theorem map_mul_right_nhds_one {G : Type w} [] [] [] (x : G) :
Filter.map (fun (x_1 : G) => x_1 * x) (nhds 1) = nhds x
theorem Filter.HasBasis.nhds_of_zero {G : Type w} [] [] {ι : Sort u_1} {p : ιProp} {s : ιSet G} (hb : (nhds 0).HasBasis p s) (x : G) :
(nhds x).HasBasis p fun (i : ι) => {y : G | y - x s i}
theorem Filter.HasBasis.nhds_of_one {G : Type w} [] [] [] {ι : Sort u_1} {p : ιProp} {s : ιSet G} (hb : (nhds 1).HasBasis p s) (x : G) :
(nhds x).HasBasis p fun (i : ι) => {y : G | y / x s i}
theorem mem_closure_iff_nhds_zero {G : Type w} [] [] {x : G} {s : Set G} :
x Unhds 0, ys, y - x U
theorem mem_closure_iff_nhds_one {G : Type w} [] [] [] {x : G} {s : Set G} :
x Unhds 1, ys, y / x U
theorem continuous_of_continuousAt_zero {G : Type w} [] [] {M : Type u_1} {hom : Type u_2} [] [] [] [FunLike hom G M] [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} [] [] [] [FunLike hom G M] [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.

@[inline]
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
Equations
• =
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 : G × H) => (f x.1) x.2) (0, 0)) (hl : ∀ (x : G), ContinuousAt (⇑(f x)) 0) (hr : ∀ (y : H), ContinuousAt (fun (x : G) => (f x) y) 0) :
Continuous fun (x : G × H) => (f x.1) x.2
theorem continuous_of_continuousAt_one₂ {G : Type w} [] [] [] {H : Type u_1} {M : Type u_2} [] [] [] [] [] [] (f : G →* H →* M) (hf : ContinuousAt (fun (x : G × H) => (f x.1) x.2) (1, 1)) (hl : ∀ (x : G), ContinuousAt (⇑(f x)) 1) (hr : ∀ (y : H), ContinuousAt (fun (x : G) => (f x) y) 1) :
Continuous fun (x : G × H) => (f x.1) x.2
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 : G) => -x) (nhds 0) (nhds 0)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun (x : G) => x₀ + x) (nhds 0)) (hconj : ∀ (x₀ : G), Filter.Tendsto (fun (x : G) => x₀ + x + -x₀) (nhds 0) (nhds 0)) :
theorem ContinuousInv.of_nhds_one {G : Type u_1} [] [] (hinv : Filter.Tendsto (fun (x : G) => x⁻¹) (nhds 1) (nhds 1)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun (x : G) => x₀ * x) (nhds 1)) (hconj : ∀ (x₀ : G), Filter.Tendsto (fun (x : G) => x₀ * x * x₀⁻¹) (nhds 1) (nhds 1)) :
theorem TopologicalAddGroup.of_nhds_zero' {G : Type u} [] [] (hmul : Filter.Tendsto (Function.uncurry fun (x x_1 : G) => x + x_1) (nhds 0 ×ˢ nhds 0) (nhds 0)) (hinv : Filter.Tendsto (fun (x : G) => -x) (nhds 0) (nhds 0)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun (x : G) => x₀ + x) (nhds 0)) (hright : ∀ (x₀ : G), nhds x₀ = Filter.map (fun (x : G) => x + x₀) (nhds 0)) :
theorem TopologicalGroup.of_nhds_one' {G : Type u} [] [] (hmul : Filter.Tendsto (Function.uncurry fun (x x_1 : G) => x * x_1) (nhds 1 ×ˢ nhds 1) (nhds 1)) (hinv : Filter.Tendsto (fun (x : G) => x⁻¹) (nhds 1) (nhds 1)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun (x : G) => x₀ * x) (nhds 1)) (hright : ∀ (x₀ : G), nhds x₀ = Filter.map (fun (x : G) => x * x₀) (nhds 1)) :
theorem TopologicalAddGroup.of_nhds_zero {G : Type u} [] [] (hmul : Filter.Tendsto (Function.uncurry fun (x x_1 : G) => x + x_1) (nhds 0 ×ˢ nhds 0) (nhds 0)) (hinv : Filter.Tendsto (fun (x : G) => -x) (nhds 0) (nhds 0)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun (x : G) => x₀ + x) (nhds 0)) (hconj : ∀ (x₀ : G), Filter.Tendsto (fun (x : G) => x₀ + x + -x₀) (nhds 0) (nhds 0)) :
theorem TopologicalGroup.of_nhds_one {G : Type u} [] [] (hmul : Filter.Tendsto (Function.uncurry fun (x x_1 : G) => x * x_1) (nhds 1 ×ˢ nhds 1) (nhds 1)) (hinv : Filter.Tendsto (fun (x : G) => x⁻¹) (nhds 1) (nhds 1)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun (x : G) => x₀ * x) (nhds 1)) (hconj : ∀ (x₀ : G), Filter.Tendsto (fun (x : G) => 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 : G) => x + x_1) (nhds 0 ×ˢ nhds 0) (nhds 0)) (hinv : Filter.Tendsto (fun (x : G) => -x) (nhds 0) (nhds 0)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun (x : G) => x₀ + x) (nhds 0)) :
theorem TopologicalGroup.of_comm_of_nhds_one {G : Type u} [] [] (hmul : Filter.Tendsto (Function.uncurry fun (x x_1 : G) => x * x_1) (nhds 1 ×ˢ nhds 1) (nhds 1)) (hinv : Filter.Tendsto (fun (x : G) => x⁻¹) (nhds 1) (nhds 1)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun (x : G) => x₀ * x) (nhds 1)) :
Equations
• = instTopologicalSpaceQuotient
instance QuotientGroup.Quotient.topologicalSpace {G : Type u_1} [] [] (N : ) :
Equations
• = instTopologicalSpaceQuotient
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 : ) [N.Normal] :
Equations
• =
instance topologicalGroup_quotient {G : Type w} [] [] [] (N : ) [N.Normal] :
Equations
• =
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 : Set G), (nhds 0).HasAntitoneBasis 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 : Set G), (nhds 1).HasAntitoneBasis 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 : N.Normal) :
(nhds 0).IsCountablyGenerated

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

Equations
• =
instance QuotientGroup.nhds_one_isCountablyGenerated (G : Type w) [] [] [] (N : ) (n : N.Normal) :
(nhds 1).IsCountablyGenerated

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

Equations
• =
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
theorem ContinuousSub.continuous_sub {G : Type u_1} [] [Sub G] [self : ] :
Continuous fun (p : G × G) => p.1 - p.2
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
theorem ContinuousDiv.continuous_div' {G : Type u_1} [] [Div G] [self : ] :
Continuous fun (p : G × G) => p.1 / p.2
@[instance 100]
Equations
• =
@[instance 100]
instance TopologicalGroup.to_continuousDiv {G : Type w} [] [] [] :
Equations
• =
theorem Filter.Tendsto.sub {G : Type w} {α : Type u} [] [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' {G : Type w} {α : Type u} [] [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 {G : Type w} {α : Type u} [] [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' {G : Type w} {α : Type u} [] [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_const_sub_iff {α : Type u} {G : Type u_1} [] [] [] (b : G) {c : G} {f : αG} {l : } :
Filter.Tendsto (fun (k : α) => b - f k) l (nhds (b - c)) Filter.Tendsto f l (nhds c)
theorem Filter.tendsto_const_div_iff {α : Type u} {G : Type u_1} [] [] [] (b : G) {c : G} {f : αG} {l : } :
Filter.Tendsto (fun (k : α) => b / f k) l (nhds (b / c)) Filter.Tendsto f l (nhds c)
theorem Filter.Tendsto.sub_const {G : Type w} {α : Type u} [] [Sub G] [] {c : G} {f : αG} {l : } (h : Filter.Tendsto f l (nhds c)) (b : G) :
Filter.Tendsto (fun (x : α) => f x - b) l (nhds (c - b))
theorem Filter.Tendsto.div_const' {G : Type w} {α : Type u} [] [Div G] [] {c : G} {f : αG} {l : } (h : Filter.Tendsto f l (nhds c)) (b : G) :
Filter.Tendsto (fun (x : α) => f x / b) l (nhds (c / b))
theorem Filter.tendsto_div_const_iff {α : Type u} {G : Type u_1} [] [] {b : G} (hb : b 0) {c : G} {f : αG} {l : } :
Filter.Tendsto (fun (x : α) => f x / b) l (nhds (c / b)) Filter.Tendsto f l (nhds c)
theorem Filter.tendsto_sub_const_iff {α : Type u} {G : Type u_1} [] [] [] (b : G) {c : G} {f : αG} {l : } :
Filter.Tendsto (fun (x : α) => f x - b) l (nhds (c - b)) Filter.Tendsto f l (nhds c)
theorem Continuous.sub {G : Type w} {α : Type u} [] [Sub G] [] [] {f : αG} {g : αG} (hf : ) (hg : ) :
Continuous fun (x : α) => f x - g x
theorem Continuous.div' {G : Type w} {α : Type u} [] [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 (x : G) => a - x
theorem continuous_div_left' {G : Type w} [] [Div G] [] (a : G) :
Continuous fun (x : G) => a / x
theorem continuous_sub_right {G : Type w} [] [Sub G] [] (a : G) :
Continuous fun (x : G) => x - a
theorem continuous_div_right' {G : Type w} [] [Div G] [] (a : G) :
Continuous fun (x : G) => x / a
theorem ContinuousAt.sub {G : Type w} {α : Type u} [] [Sub G] [] [] {f : αG} {g : αG} {x : α} (hf : ) (hg : ) :
ContinuousAt (fun (x : α) => f x - g x) x
theorem ContinuousAt.div' {G : Type w} {α : Type u} [] [Div G] [] [] {f : αG} {g : αG} {x : α} (hf : ) (hg : ) :
ContinuousAt (fun (x : α) => f x / g x) x
theorem ContinuousWithinAt.sub {G : Type w} {α : Type u} [] [Sub G] [] [] {f : αG} {g : αG} {s : Set α} {x : α} (hf : ) (hg : ) :
ContinuousWithinAt (fun (x : α) => f x - g x) s x
theorem ContinuousWithinAt.div' {G : Type w} {α : Type u} [] [Div G] [] [] {f : αG} {g : αG} {s : Set α} {x : α} (hf : ) (hg : ) :
ContinuousWithinAt (fun (x : α) => f x / g x) s x
theorem ContinuousOn.sub {G : Type w} {α : Type u} [] [Sub G] [] [] {f : αG} {g : αG} {s : Set α} (hf : ) (hg : ) :
ContinuousOn (fun (x : α) => f x - g x) s
theorem ContinuousOn.div' {G : Type w} {α : Type u} [] [Div G] [] [] {f : αG} {g : αG} {s : Set α} (hf : ) (hg : ) :
ContinuousOn (fun (x : α) => f x / g x) s
theorem Homeomorph.subLeft.proof_2 {G : Type u_1} [] [] (x : G) :
Continuous fun (x_1 : G) => -x_1 + x
def Homeomorph.subLeft {G : Type w} [] [] (x : G) :
G ≃ₜ G

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

Equations
• = let __src := ; { toEquiv := __src, continuous_toFun := , continuous_invFun := }
Instances For
theorem Homeomorph.subLeft.proof_1 {G : Type u_1} [] [] (x : G) :
Continuous fun (x_1 : G) => x - x_1
@[simp]
theorem Homeomorph.divLeft_apply {G : Type w} [] [] [] (x : G) (b : G) :
b = x / b
@[simp]
theorem Homeomorph.subLeft_apply {G : Type w} [] [] (x : G) (b : G) :
b = x - b
@[simp]
theorem Homeomorph.divLeft_symm_apply {G : Type w} [] [] [] (x : G) (b : G) :
.symm b = b⁻¹ * x
@[simp]
theorem Homeomorph.subLeft_symm_apply {G : Type w} [] [] (x : G) (b : G) :
.symm b = -b + x
def Homeomorph.divLeft {G : Type w} [] [] [] (x : G) :
G ≃ₜ G

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

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

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

Equations
• = let __src := ; { toEquiv := __src, continuous_toFun := , continuous_invFun := }
Instances For
theorem Homeomorph.subRight.proof_1 {G : Type u_1} [] [] (x : G) :
Continuous fun (x_1 : G) => id x_1 - 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) :
.symm b = b * x
@[simp]
theorem Homeomorph.subRight_symm_apply {G : Type w} [] [] (x : G) (b : G) :
.symm 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.

Equations
• = let __src := ; { toEquiv := __src, continuous_toFun := , continuous_invFun := }
Instances For
theorem isOpenMap_sub_right {G : Type w} [] [] (a : G) :
IsOpenMap fun (x : G) => x - a
theorem isOpenMap_div_right {G : Type w} [] [] [] (a : G) :
IsOpenMap fun (x : G) => x / a
theorem isClosedMap_sub_right {G : Type w} [] [] (a : G) :
IsClosedMap fun (x : G) => x - a
theorem isClosedMap_div_right {G : Type w} [] [] [] (a : G) :
IsClosedMap fun (x : G) => x / a
theorem tendsto_sub_nhds_zero_iff {G : Type w} [] [] {α : Type u_1} {l : } {x : G} {u : αG} :
Filter.Tendsto (fun (x_1 : α) => u x_1 - 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 (x_1 : α) => u x_1 / x) l (nhds 1) Filter.Tendsto u l (nhds x)
theorem nhds_translation_sub {G : Type w} [] [] (x : G) :
Filter.comap (fun (x_1 : G) => x_1 - x) (nhds 0) = nhds x
theorem nhds_translation_div {G : Type w} [] [] [] (x : G) :
Filter.comap (fun (x_1 : G) => x_1 / 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 subset_interior_vadd {α : Type u} {β : Type v} [] [] [] [] {s : Set α} {t : Set β} [] :
theorem subset_interior_smul {α : Type u} {β : Type v} [] [] [] [] {s : Set α} {t : Set β} [] :
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 {G : Type w} [] [] {s : Set G} {t : Set G} (ht : ) :
IsOpen (s - t)
theorem IsOpen.div_left {G : Type w} [] [] [] {s : Set G} {t : Set G} (ht : ) :
IsOpen (s / t)
theorem IsOpen.sub_right {G : Type w} [] [] {s : Set G} {t : Set G} (hs : ) :
IsOpen (s - t)
theorem IsOpen.div_right {G : Type w} [] [] [] {s : Set G} {t : Set G} (hs : ) :
IsOpen (s / t)
theorem subset_interior_sub_left {G : Type w} [] [] {s : Set G} {t : Set G} :
- t interior (s - t)
theorem subset_interior_div_left {G : Type w} [] [] [] {s : Set G} {t : Set G} :
/ t interior (s / t)
theorem subset_interior_sub_right {G : Type w} [] [] {s : Set G} {t : Set G} :
s - interior (s - t)
theorem subset_interior_div_right {G : Type w} [] [] [] {s : Set G} {t : Set G} :
s / interior (s / t)
theorem subset_interior_sub {G : Type w} [] [] {s : Set G} {t : Set G} :
interior (s - t)
theorem subset_interior_div {G : Type w} [] [] [] {s : Set G} {t : Set G} :
interior (s / t)
theorem IsOpen.add_closure {G : Type w} [] [] {s : Set G} (hs : ) (t : Set G) :
s + = s + t
theorem IsOpen.mul_closure {G : Type w} [] [] [] {s : Set G} (hs : ) (t : Set G) :
s * = s * t
theorem IsOpen.closure_add {G : Type w} [] [] {t : Set G} (ht : ) (s : Set G) :
+ t = s + t
theorem IsOpen.closure_mul {G : Type w} [] [] [] {t : Set G} (ht : ) (s : Set G) :
* t = s * t
theorem IsOpen.sub_closure {G : Type w} [] [] {s : Set G} (hs : ) (t : Set G) :
s - = s - t
theorem IsOpen.div_closure {G : Type w} [] [] [] {s : Set G} (hs : ) (t : Set G) :
s / = s / t
theorem IsOpen.closure_sub {G : Type w} [] [] {t : Set G} (ht : ) (s : Set G) :
- t = s - t
theorem IsOpen.closure_div {G : Type w} [] [] [] {t : Set G} (ht : ) (s : Set G) :
/ t = s / t
theorem IsClosed.add_left_of_isCompact {G : Type w} [] [] {s : Set G} {t : Set G} (ht : ) (hs : ) :
IsClosed (s + t)
theorem IsClosed.mul_left_of_isCompact {G : Type w} [] [] [] {s : Set G} {t : Set G} (ht : ) (hs : ) :
IsClosed (s * t)
theorem IsClosed.add_right_of_isCompact {G : Type w} [] [] {s : Set G} {t : Set G} (ht : ) (hs : ) :
IsClosed (t + s)
theorem IsClosed.mul_right_of_isCompact {G : Type w} [] [] [] {s : Set G} {t : Set G} (ht : ) (hs : ) :
IsClosed (t * s)
theorem QuotientAddGroup.isClosedMap_coe {G : Type w} [] [] {H : } (hH : ) :
theorem QuotientGroup.isClosedMap_coe {G : Type w} [] [] [] {H : } (hH : ) :
IsClosedMap QuotientGroup.mk
theorem subset_add_closure_zero {G : Type u_1} [] [] (s : Set G) :
s s + closure {0}
theorem subset_mul_closure_one {G : Type u_1} [] [] (s : Set G) :
s s * closure {1}
theorem IsCompact.add_closure_zero_eq_closure {G : Type w} [] [] {K : Set G} (hK : ) :
K + closure {0} =
theorem IsCompact.mul_closure_one_eq_closure {G : Type w} [] [] [] {K : Set G} (hK : ) :
K * closure {1} =
theorem IsClosed.add_closure_zero_eq {G : Type w} [] [] {F : Set G} (hF : ) :
F + closure {0} = F
theorem IsClosed.mul_closure_one_eq {G : Type w} [] [] [] {F : Set G} (hF : ) :
F * closure {1} = F
theorem compl_add_closure_zero_eq {G : Type w} [] [] {t : Set G} (ht : t + closure {0} = t) :
t + closure {0} = t
theorem compl_mul_closure_one_eq {G : Type w} [] [] [] {t : Set G} (ht : t * closure {1} = t) :
t * closure {1} = t
theorem compl_add_closure_zero_eq_iff {G : Type w} [] [] {t : Set G} :
t + closure {0} = t t + closure {0} = t
theorem compl_mul_closure_one_eq_iff {G : Type w} [] [] [] {t : Set G} :
t * closure {1} = t t * closure {1} = t
theorem IsOpen.add_closure_zero_eq {G : Type w} [] [] {U : Set G} (hU : ) :
U + closure {0} = U
theorem IsOpen.mul_closure_one_eq {G : Type w} [] [] [] {U : Set G} (hU : ) :
U * closure {1} = U
theorem TopologicalAddGroup.t1Space (G : Type w) [] [] [] (h : IsClosed {0}) :