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} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (a : G) : Continuous fun (x : G) => ↑(toAddUnits a) + x

def Homeomorph.addLeft {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (a : G) : G ≃ₜ G

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

Equations

• Homeomorph.addLeft a = { toEquiv := Equiv.addLeft a, continuous_toFun := ⋯, continuous_invFun := ⋯ }

theorem Homeomorph.addLeft.proof_2 {G : Type u_1} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (a : G) : Continuous fun (x : G) => ↑(-toAddUnits a) + x

def Homeomorph.mulLeft {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] (a : G) : G ≃ₜ G

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

Equations

• Homeomorph.mulLeft a = { toEquiv := Equiv.mulLeft a, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.coe_addLeft {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (a : G) : ⇑(Homeomorph.addLeft a) = fun (x : G) => a + x

@[simp]

theorem Homeomorph.coe_mulLeft {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] (a : G) : ⇑(Homeomorph.mulLeft a) = fun (x : G) => a * x

theorem Homeomorph.addLeft_symm {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (a : G) : (Homeomorph.addLeft a).symm = Homeomorph.addLeft (-a)

theorem Homeomorph.mulLeft_symm {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] (a : G) : (Homeomorph.mulLeft a).symm = Homeomorph.mulLeft a⁻¹

theorem isOpenMap_add_left {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (a : G) : IsOpenMap fun (x : G) => a + x

theorem isOpenMap_mul_left {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] (a : G) : IsOpenMap fun (x : G) => a * x

theorem IsOpen.left_addCoset {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] {U : Set G} (h : IsOpen U) (x : G) : IsOpen (x +ᵥ U)

theorem IsOpen.leftCoset {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] {U : Set G} (h : IsOpen U) (x : G) : IsOpen (x • U)

theorem isClosedMap_add_left {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (a : G) : IsClosedMap fun (x : G) => a + x

theorem isClosedMap_mul_left {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] (a : G) : IsClosedMap fun (x : G) => a * x

theorem IsClosed.left_addCoset {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] {U : Set G} (h : IsClosed U) (x : G) : IsClosed (x +ᵥ U)

theorem IsClosed.leftCoset {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] {U : Set G} (h : IsClosed U) (x : G) : IsClosed (x • U)

def Homeomorph.addRight {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (a : G) : G ≃ₜ G

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

Equations

• Homeomorph.addRight a = { toEquiv := Equiv.addRight a, continuous_toFun := ⋯, continuous_invFun := ⋯ }

theorem Homeomorph.addRight.proof_2 {G : Type u_1} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (a : G) : Continuous fun (x : G) => id x + ↑(-toAddUnits a)

theorem Homeomorph.addRight.proof_1 {G : Type u_1} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (a : G) : Continuous fun (x : G) => id x + ↑(toAddUnits a)

def Homeomorph.mulRight {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] (a : G) : G ≃ₜ G

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

Equations

• Homeomorph.mulRight a = { toEquiv := Equiv.mulRight a, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.coe_addRight {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (a : G) : ⇑(Homeomorph.addRight a) = fun (x : G) => x + a

@[simp]

theorem Homeomorph.coe_mulRight {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] (a : G) : ⇑(Homeomorph.mulRight a) = fun (x : G) => x * a

theorem Homeomorph.addRight_symm {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (a : G) : (Homeomorph.addRight a).symm = Homeomorph.addRight (-a)

theorem Homeomorph.mulRight_symm {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] (a : G) : (Homeomorph.mulRight a).symm = Homeomorph.mulRight a⁻¹

theorem isOpenMap_add_right {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (a : G) : IsOpenMap fun (x : G) => x + a

theorem isOpenMap_mul_right {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] (a : G) : IsOpenMap fun (x : G) => x * a

theorem IsOpen.right_addCoset {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] {U : Set G} (h : IsOpen U) (x : G) : IsOpen (AddOpposite.op x +ᵥ U)

theorem IsOpen.rightCoset {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] {U : Set G} (h : IsOpen U) (x : G) : IsOpen (MulOpposite.op x • U)

theorem isClosedMap_add_right {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (a : G) : IsClosedMap fun (x : G) => x + a

theorem isClosedMap_mul_right {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] (a : G) : IsClosedMap fun (x : G) => x * a

theorem IsClosed.right_addCoset {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] {U : Set G} (h : IsClosed U) (x : G) : IsClosed (AddOpposite.op x +ᵥ U)

theorem IsClosed.rightCoset {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] {U : Set G} (h : IsClosed U) (x : G) : IsClosed (MulOpposite.op x • U)

theorem discreteTopology_of_isOpen_singleton_zero {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (h : IsOpen {0}) : DiscreteTopology G

theorem discreteTopology_of_isOpen_singleton_one {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] (h : IsOpen {1}) : DiscreteTopology G

theorem discreteTopology_iff_isOpen_singleton_zero {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] : DiscreteTopology G ↔ IsOpen {0}

theorem discreteTopology_iff_isOpen_singleton_one {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] : DiscreteTopology G ↔ IsOpen {1}

ContinuousInv and ContinuousNeg

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

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

• continuous_neg : Continuous fun (a : G) => -a

theorem ContinuousNeg.continuous_neg {G : Type u} : ∀ {inst : TopologicalSpace G} {inst_1 : Neg G} [self : ContinuousNeg G], Continuous fun (a : G) => -a

class ContinuousInv (G : Type u) [TopologicalSpace G] [Inv G] : Prop

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

• continuous_inv : Continuous fun (a : G) => a⁻¹

theorem ContinuousInv.continuous_inv {G : Type u} : ∀ {inst : TopologicalSpace G} {inst_1 : Inv G} [self : ContinuousInv G], Continuous fun (a : G) => a⁻¹

theorem ContinuousNeg.induced {α : Type u_1} {β : Type u_2} {F : Type u_3} [FunLike F α β] [AddGroup α] [AddGroup β] [AddMonoidHomClass F α β] [tβ : TopologicalSpace β] [ContinuousNeg β] (f : F) : ContinuousNeg α

theorem ContinuousInv.induced {α : Type u_1} {β : Type u_2} {F : Type u_3} [FunLike F α β] [Group α] [Group β] [MonoidHomClass F α β] [tβ : TopologicalSpace β] [ContinuousInv β] (f : F) : ContinuousInv α

theorem Specializes.neg {G : Type w} [TopologicalSpace G] [Neg G] [ContinuousNeg G] {x : G} {y : G} (h : x ⤳ y) : (-x) ⤳ (-y)

theorem Specializes.inv {G : Type w} [TopologicalSpace G] [Inv G] [ContinuousInv G] {x : G} {y : G} (h : x ⤳ y) : x⁻¹ ⤳ y⁻¹

theorem Inseparable.neg {G : Type w} [TopologicalSpace G] [Neg G] [ContinuousNeg G] {x : G} {y : G} (h : Inseparable x y) : Inseparable (-x) (-y)

theorem Inseparable.inv {G : Type w} [TopologicalSpace G] [Inv G] [ContinuousInv G] {x : G} {y : G} (h : Inseparable x y) : Inseparable x⁻¹ y⁻¹

theorem Specializes.zsmul {G : Type u_1} [SubNegMonoid G] [TopologicalSpace G] [ContinuousAdd G] [ContinuousNeg G] {x : G} {y : G} (h : x ⤳ y) (m : ℤ) : (m • x) ⤳ (m • y)

theorem Specializes.zpow {G : Type u_1} [DivInvMonoid G] [TopologicalSpace G] [ContinuousMul G] [ContinuousInv G] {x : G} {y : G} (h : x ⤳ y) (m : ℤ) : (x ^ m) ⤳ (y ^ m)

theorem Inseparable.zsmul {G : Type u_1} [SubNegMonoid G] [TopologicalSpace G] [ContinuousAdd G] [ContinuousNeg G] {x : G} {y : G} (h : Inseparable x y) (m : ℤ) : Inseparable (m • x) (m • y)

theorem Inseparable.zpow {G : Type u_1} [DivInvMonoid G] [TopologicalSpace G] [ContinuousMul G] [ContinuousInv G] {x : G} {y : G} (h : Inseparable x y) (m : ℤ) : Inseparable (x ^ m) (y ^ m)

instance instContinuousNegULift {G : Type w} [TopologicalSpace G] [Neg G] [ContinuousNeg G] : ContinuousNeg (ULift.{u_1, w} G)

Equations

• ⋯ = ⋯

instance instContinuousInvULift {G : Type w} [TopologicalSpace G] [Inv G] [ContinuousInv G] : ContinuousInv (ULift.{u_1, w} G)

Equations

• ⋯ = ⋯

theorem continuousOn_neg {G : Type w} [TopologicalSpace G] [Neg G] [ContinuousNeg G] {s : Set G} : ContinuousOn Neg.neg s

theorem continuousOn_inv {G : Type w} [TopologicalSpace G] [Inv G] [ContinuousInv G] {s : Set G} : ContinuousOn Inv.inv s

theorem continuousWithinAt_neg {G : Type w} [TopologicalSpace G] [Neg G] [ContinuousNeg G] {s : Set G} {x : G} : ContinuousWithinAt Neg.neg s x

theorem continuousWithinAt_inv {G : Type w} [TopologicalSpace G] [Inv G] [ContinuousInv G] {s : Set G} {x : G} : ContinuousWithinAt Inv.inv s x

theorem continuousAt_neg {G : Type w} [TopologicalSpace G] [Neg G] [ContinuousNeg G] {x : G} : ContinuousAt Neg.neg x

theorem continuousAt_inv {G : Type w} [TopologicalSpace G] [Inv G] [ContinuousInv G] {x : G} : ContinuousAt Inv.inv x

theorem tendsto_neg {G : Type w} [TopologicalSpace G] [Neg G] [ContinuousNeg G] (a : G) : Filter.Tendsto Neg.neg (nhds a) (nhds (-a))

theorem tendsto_inv {G : Type w} [TopologicalSpace G] [Inv G] [ContinuousInv G] (a : G) : Filter.Tendsto Inv.inv (nhds a) (nhds a⁻¹)

theorem Filter.Tendsto.neg {G : Type w} {α : Type u} [TopologicalSpace G] [Neg G] [ContinuousNeg G] {f : α → G} {l : Filter α} {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} [TopologicalSpace G] [Inv G] [ContinuousInv G] {f : α → G} {l : Filter α} {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} [TopologicalSpace G] [Neg G] [ContinuousNeg G] [TopologicalSpace α] {f : α → G} (hf : Continuous f) : Continuous fun (x : α) => -f x

theorem Continuous.inv {G : Type w} {α : Type u} [TopologicalSpace G] [Inv G] [ContinuousInv G] [TopologicalSpace α] {f : α → G} (hf : Continuous f) : Continuous fun (x : α) => (f x)⁻¹

theorem ContinuousAt.neg {G : Type w} {α : Type u} [TopologicalSpace G] [Neg G] [ContinuousNeg G] [TopologicalSpace α] {f : α → G} {x : α} (hf : ContinuousAt f x) : ContinuousAt (fun (x : α) => -f x) x

theorem ContinuousAt.inv {G : Type w} {α : Type u} [TopologicalSpace G] [Inv G] [ContinuousInv G] [TopologicalSpace α] {f : α → G} {x : α} (hf : ContinuousAt f x) : ContinuousAt (fun (x : α) => (f x)⁻¹) x

theorem ContinuousOn.neg {G : Type w} {α : Type u} [TopologicalSpace G] [Neg G] [ContinuousNeg G] [TopologicalSpace α] {f : α → G} {s : Set α} (hf : ContinuousOn f s) : ContinuousOn (fun (x : α) => -f x) s

theorem ContinuousOn.inv {G : Type w} {α : Type u} [TopologicalSpace G] [Inv G] [ContinuousInv G] [TopologicalSpace α] {f : α → G} {s : Set α} (hf : ContinuousOn f s) : ContinuousOn (fun (x : α) => (f x)⁻¹) s

theorem ContinuousWithinAt.neg {G : Type w} {α : Type u} [TopologicalSpace G] [Neg G] [ContinuousNeg G] [TopologicalSpace α] {f : α → G} {s : Set α} {x : α} (hf : ContinuousWithinAt f s x) : ContinuousWithinAt (fun (x : α) => -f x) s x

theorem ContinuousWithinAt.inv {G : Type w} {α : Type u} [TopologicalSpace G] [Inv G] [ContinuousInv G] [TopologicalSpace α] {f : α → G} {s : Set α} {x : α} (hf : ContinuousWithinAt f s x) : ContinuousWithinAt (fun (x : α) => (f x)⁻¹) s x

instance Prod.continuousNeg {G : Type w} {H : Type x} [TopologicalSpace G] [Neg G] [ContinuousNeg G] [TopologicalSpace H] [Neg H] [ContinuousNeg H] : ContinuousNeg (G × H)

Equations

• ⋯ = ⋯

instance Prod.continuousInv {G : Type w} {H : Type x} [TopologicalSpace G] [Inv G] [ContinuousInv G] [TopologicalSpace H] [Inv H] [ContinuousInv H] : ContinuousInv (G × 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} [TopologicalSpace G] [Neg G] [ContinuousNeg 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} [TopologicalSpace G] [Inv G] [ContinuousInv 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} [TopologicalSpace H] [Neg H] [DiscreteTopology H] : ContinuousNeg H

Equations

• ⋯ = ⋯

@[instance 100]

instance continuousInv_of_discreteTopology {H : Type x} [TopologicalSpace H] [Inv H] [DiscreteTopology H] : ContinuousInv H

Equations

• ⋯ = ⋯

theorem isClosed_setOf_map_neg (G₁ : Type u_2) (G₂ : Type u_3) [TopologicalSpace G₂] [T2Space G₂] [Neg G₁] [Neg G₂] [ContinuousNeg G₂] : IsClosed {f : G₁ → G₂ | ∀ (x : G₁), f (-x) = -f x}

theorem isClosed_setOf_map_inv (G₁ : Type u_2) (G₂ : Type u_3) [TopologicalSpace G₂] [T2Space G₂] [Inv G₁] [Inv G₂] [ContinuousInv G₂] : IsClosed {f : G₁ → G₂ | ∀ (x : G₁), f x⁻¹ = (f x)⁻¹}

instance instContinuousNegAdditiveOfContinuousInv {H : Type x} [TopologicalSpace H] [Inv H] [ContinuousInv H] : ContinuousNeg (Additive H)

Equations

• ⋯ = ⋯

instance instContinuousInvMultiplicativeOfContinuousNeg {H : Type x} [TopologicalSpace H] [Neg H] [ContinuousNeg H] : ContinuousInv (Multiplicative H)

Equations

• ⋯ = ⋯

theorem IsCompact.neg {G : Type w} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] {s : Set G} (hs : IsCompact s) : IsCompact (-s)

theorem IsCompact.inv {G : Type w} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] {s : Set G} (hs : IsCompact s) : IsCompact s⁻¹

theorem Homeomorph.neg.proof_1 (G : Type u_1) [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] : Continuous fun (a : G) => -a

def Homeomorph.neg (G : Type u_1) [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] : G ≃ₜ G

Negation in a topological group as a homeomorphism.

Equations

• Homeomorph.neg G = { toEquiv := Equiv.neg G, continuous_toFun := ⋯, continuous_invFun := ⋯ }

def Homeomorph.inv (G : Type u_1) [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] : G ≃ₜ G

Inversion in a topological group as a homeomorphism.

Equations

• Homeomorph.inv G = { toEquiv := Equiv.inv G, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.coe_neg {G : Type u_1} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] : ⇑(Homeomorph.neg G) = Neg.neg

@[simp]

theorem Homeomorph.coe_inv {G : Type u_1} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] : ⇑(Homeomorph.inv G) = Inv.inv

theorem nhds_neg (G : Type w) [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] (a : G) : nhds (-a) = -nhds a

theorem nhds_inv (G : Type w) [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] (a : G) : nhds a⁻¹ = (nhds a)⁻¹

theorem isOpenMap_neg (G : Type w) [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] : IsOpenMap Neg.neg

theorem isOpenMap_inv (G : Type w) [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] : IsOpenMap Inv.inv

theorem isClosedMap_neg (G : Type w) [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] : IsClosedMap Neg.neg

theorem isClosedMap_inv (G : Type w) [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] : IsClosedMap Inv.inv

theorem IsOpen.neg {G : Type w} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] {s : Set G} (hs : IsOpen s) : IsOpen (-s)

theorem IsOpen.inv {G : Type w} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] {s : Set G} (hs : IsOpen s) : IsOpen s⁻¹

theorem IsClosed.neg {G : Type w} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] {s : Set G} (hs : IsClosed s) : IsClosed (-s)

theorem IsClosed.inv {G : Type w} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] {s : Set G} (hs : IsClosed s) : IsClosed s⁻¹

theorem neg_closure {G : Type w} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] (s : Set G) : -closure s = closure (-s)

theorem inv_closure {G : Type w} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] (s : Set G) : (closure s)⁻¹ = closure s⁻¹

@[simp]

theorem continuous_neg_iff {G : Type w} {α : Type u} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] [TopologicalSpace α] {f : α → G} : Continuous (-f) ↔ Continuous f

@[simp]

theorem continuous_inv_iff {G : Type w} {α : Type u} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] [TopologicalSpace α] {f : α → G} : Continuous f⁻¹ ↔ Continuous f

@[simp]

theorem continuousAt_neg_iff {G : Type w} {α : Type u} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] [TopologicalSpace α] {f : α → G} {x : α} : ContinuousAt (-f) x ↔ ContinuousAt f x

@[simp]

theorem continuousAt_inv_iff {G : Type w} {α : Type u} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] [TopologicalSpace α] {f : α → G} {x : α} : ContinuousAt f⁻¹ x ↔ ContinuousAt f x

@[simp]

theorem continuousOn_neg_iff {G : Type w} {α : Type u} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] [TopologicalSpace α] {f : α → G} {s : Set α} : ContinuousOn (-f) s ↔ ContinuousOn f s

@[simp]

theorem continuousOn_inv_iff {G : Type w} {α : Type u} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] [TopologicalSpace α] {f : α → G} {s : Set α} : ContinuousOn f⁻¹ s ↔ ContinuousOn f s

theorem Continuous.of_inv {G : Type w} {α : Type u} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] [TopologicalSpace α] {f : α → G} : Continuous f⁻¹ → Continuous f

Alias of the forward direction of continuous_inv_iff.

theorem Continuous.of_neg {G : Type w} {α : Type u} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] [TopologicalSpace α] {f : α → G} : Continuous (-f) → Continuous f

theorem ContinuousAt.of_inv {G : Type w} {α : Type u} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] [TopologicalSpace α] {f : α → G} {x : α} : ContinuousAt f⁻¹ x → ContinuousAt f x

Alias of the forward direction of continuousAt_inv_iff.

theorem ContinuousAt.of_neg {G : Type w} {α : Type u} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] [TopologicalSpace α] {f : α → G} {x : α} : ContinuousAt (-f) x → ContinuousAt f x

theorem ContinuousOn.of_inv {G : Type w} {α : Type u} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] [TopologicalSpace α] {f : α → G} {s : Set α} : ContinuousOn f⁻¹ s → ContinuousOn f s

Alias of the forward direction of continuousOn_inv_iff.

theorem ContinuousOn.of_neg {G : Type w} {α : Type u} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] [TopologicalSpace α] {f : α → G} {s : Set α} : ContinuousOn (-f) s → ContinuousOn f s

theorem continuousNeg_sInf {G : Type w} [Neg G] {ts : Set (TopologicalSpace G)} (h : ∀ t ∈ ts, ContinuousNeg G) : ContinuousNeg G

theorem continuousInv_sInf {G : Type w} [Inv G] {ts : Set (TopologicalSpace G)} (h : ∀ t ∈ ts, ContinuousInv G) : ContinuousInv G

theorem continuousNeg_iInf {G : Type w} {ι' : Sort u_1} [Neg G] {ts' : ι' → TopologicalSpace G} (h' : ∀ (i : ι'), ContinuousNeg G) : ContinuousNeg G

theorem continuousInv_iInf {G : Type w} {ι' : Sort u_1} [Inv G] {ts' : ι' → TopologicalSpace G} (h' : ∀ (i : ι'), ContinuousInv G) : ContinuousInv G

theorem continuousNeg_inf {G : Type w} [Neg G] {t₁ : TopologicalSpace G} {t₂ : TopologicalSpace G} (h₁ : ContinuousNeg G) (h₂ : ContinuousNeg G) : ContinuousNeg G

theorem continuousInv_inf {G : Type w} [Inv G] {t₁ : TopologicalSpace G} {t₂ : TopologicalSpace G} (h₁ : ContinuousInv G) (h₂ : ContinuousInv G) : ContinuousInv G

theorem IsInducing.continuousNeg {G : Type u_1} {H : Type u_2} [Neg G] [Neg H] [TopologicalSpace G] [TopologicalSpace H] [ContinuousNeg H] {f : G → H} (hf : IsInducing f) (hf_inv : ∀ (x : G), f (-x) = -f x) : ContinuousNeg G

theorem IsInducing.continuousInv {G : Type u_1} {H : Type u_2} [Inv G] [Inv H] [TopologicalSpace G] [TopologicalSpace H] [ContinuousInv H] {f : G → H} (hf : IsInducing f) (hf_inv : ∀ (x : G), f x⁻¹ = (f x)⁻¹) : ContinuousInv G

@[deprecated IsInducing.continuousInv]

theorem Inducing.continuousInv {G : Type u_1} {H : Type u_2} [Inv G] [Inv H] [TopologicalSpace G] [TopologicalSpace H] [ContinuousInv H] {f : G → H} (hf : IsInducing f) (hf_inv : ∀ (x : G), f x⁻¹ = (f x)⁻¹) : ContinuousInv G

Alias of IsInducing.continuousInv.

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) [TopologicalSpace G] [AddGroup G] extends ContinuousAdd , ContinuousNeg : Prop

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

class TopologicalGroup (G : Type u_1) [TopologicalSpace G] [Group G] extends ContinuousMul , ContinuousInv : Prop

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.

instance ConjAct.units_continuousConstSMul {M : Type u_1} [Monoid M] [TopologicalSpace M] [ContinuousMul M] : ContinuousConstSMul (ConjAct Mˣ) M

Equations

• ⋯ = ⋯

theorem TopologicalAddGroup.continuous_conj_sum {G : Type w} [TopologicalSpace G] [Neg G] [Add G] [ContinuousAdd G] [ContinuousNeg 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} [TopologicalSpace G] [Inv G] [Mul G] [ContinuousMul G] [ContinuousInv 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} [TopologicalSpace G] [Neg G] [Add G] [ContinuousAdd 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} [TopologicalSpace G] [Inv G] [Mul G] [ContinuousMul 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} [TopologicalSpace G] [Neg G] [Add G] [ContinuousAdd G] [ContinuousNeg 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} [TopologicalSpace G] [Inv G] [Mul G] [ContinuousMul G] [ContinuousInv 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} [TopologicalSpace G] [Group G] [TopologicalGroup G] : TopologicalGroup (ULift.{u_1, w} G)

Equations

• ⋯ = ⋯

theorem continuous_zsmul {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (z : ℤ) : Continuous fun (a : G) => z • a

theorem continuous_zpow {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (z : ℤ) : Continuous fun (a : G) => a ^ z

instance AddGroup.continuousConstSMul_int {A : Type u_1} [AddGroup A] [TopologicalSpace A] [TopologicalAddGroup A] : ContinuousConstSMul ℤ A

Equations

• ⋯ = ⋯

instance AddGroup.continuousSMul_int {A : Type u_1} [AddGroup A] [TopologicalSpace A] [TopologicalAddGroup A] : ContinuousSMul ℤ A

Equations

• ⋯ = ⋯

theorem Continuous.zsmul {G : Type w} {α : Type u} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [TopologicalSpace α] {f : α → G} (h : Continuous f) (z : ℤ) : Continuous fun (b : α) => z • f b

theorem Continuous.zpow {G : Type w} {α : Type u} [TopologicalSpace G] [Group G] [TopologicalGroup G] [TopologicalSpace α] {f : α → G} (h : Continuous f) (z : ℤ) : Continuous fun (b : α) => f b ^ z

theorem continuousOn_zsmul {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {s : Set G} (z : ℤ) : ContinuousOn (fun (x : G) => z • x) s

theorem continuousOn_zpow {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {s : Set G} (z : ℤ) : ContinuousOn (fun (x : G) => x ^ z) s

theorem continuousAt_zsmul {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (x : G) (z : ℤ) : ContinuousAt (fun (x : G) => z • x) x

theorem continuousAt_zpow {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (x : G) (z : ℤ) : ContinuousAt (fun (x : G) => x ^ z) x

theorem Filter.Tendsto.zsmul {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {α : Type u_1} {l : Filter α} {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} [TopologicalSpace G] [Group G] [TopologicalGroup G] {α : Type u_1} {l : Filter α} {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} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [TopologicalSpace α] {f : α → G} {x : α} {s : Set α} (hf : ContinuousWithinAt f s x) (z : ℤ) : ContinuousWithinAt (fun (x : α) => z • f x) s x

theorem ContinuousWithinAt.zpow {G : Type w} {α : Type u} [TopologicalSpace G] [Group G] [TopologicalGroup G] [TopologicalSpace α] {f : α → G} {x : α} {s : Set α} (hf : ContinuousWithinAt f s x) (z : ℤ) : ContinuousWithinAt (fun (x : α) => f x ^ z) s x

theorem ContinuousAt.zsmul {G : Type w} {α : Type u} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [TopologicalSpace α] {f : α → G} {x : α} (hf : ContinuousAt f x) (z : ℤ) : ContinuousAt (fun (x : α) => z • f x) x

theorem ContinuousAt.zpow {G : Type w} {α : Type u} [TopologicalSpace G] [Group G] [TopologicalGroup G] [TopologicalSpace α] {f : α → G} {x : α} (hf : ContinuousAt f x) (z : ℤ) : ContinuousAt (fun (x : α) => f x ^ z) x

theorem ContinuousOn.zsmul {G : Type w} {α : Type u} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [TopologicalSpace α] {f : α → G} {s : Set α} (hf : ContinuousOn f s) (z : ℤ) : ContinuousOn (fun (x : α) => z • f x) s

theorem ContinuousOn.zpow {G : Type w} {α : Type u} [TopologicalSpace G] [Group G] [TopologicalGroup G] [TopologicalSpace α] {f : α → G} {s : Set α} (hf : ContinuousOn f s) (z : ℤ) : ContinuousOn (fun (x : α) => f x ^ z) s

theorem tendsto_neg_nhdsWithin_Ioi {H : Type x} [TopologicalSpace H] [OrderedAddCommGroup H] [ContinuousNeg H] {a : H} : Filter.Tendsto Neg.neg (nhdsWithin a (Set.Ioi a)) (nhdsWithin (-a) (Set.Iio (-a)))

theorem tendsto_inv_nhdsWithin_Ioi {H : Type x} [TopologicalSpace H] [OrderedCommGroup H] [ContinuousInv H] {a : H} : Filter.Tendsto Inv.inv (nhdsWithin a (Set.Ioi a)) (nhdsWithin a⁻¹ (Set.Iio a⁻¹))

theorem tendsto_neg_nhdsWithin_Iio {H : Type x} [TopologicalSpace H] [OrderedAddCommGroup H] [ContinuousNeg H] {a : H} : Filter.Tendsto Neg.neg (nhdsWithin a (Set.Iio a)) (nhdsWithin (-a) (Set.Ioi (-a)))

theorem tendsto_inv_nhdsWithin_Iio {H : Type x} [TopologicalSpace H] [OrderedCommGroup H] [ContinuousInv H] {a : H} : Filter.Tendsto Inv.inv (nhdsWithin a (Set.Iio a)) (nhdsWithin a⁻¹ (Set.Ioi a⁻¹))

theorem tendsto_neg_nhdsWithin_Ioi_neg {H : Type x} [TopologicalSpace H] [OrderedAddCommGroup H] [ContinuousNeg H] {a : H} : Filter.Tendsto Neg.neg (nhdsWithin (-a) (Set.Ioi (-a))) (nhdsWithin a (Set.Iio a))

theorem tendsto_inv_nhdsWithin_Ioi_inv {H : Type x} [TopologicalSpace H] [OrderedCommGroup H] [ContinuousInv H] {a : H} : Filter.Tendsto Inv.inv (nhdsWithin a⁻¹ (Set.Ioi a⁻¹)) (nhdsWithin a (Set.Iio a))

theorem tendsto_neg_nhdsWithin_Iio_neg {H : Type x} [TopologicalSpace H] [OrderedAddCommGroup H] [ContinuousNeg H] {a : H} : Filter.Tendsto Neg.neg (nhdsWithin (-a) (Set.Iio (-a))) (nhdsWithin a (Set.Ioi a))

theorem tendsto_inv_nhdsWithin_Iio_inv {H : Type x} [TopologicalSpace H] [OrderedCommGroup H] [ContinuousInv H] {a : H} : Filter.Tendsto Inv.inv (nhdsWithin a⁻¹ (Set.Iio a⁻¹)) (nhdsWithin a (Set.Ioi a))

theorem tendsto_neg_nhdsWithin_Ici {H : Type x} [TopologicalSpace H] [OrderedAddCommGroup H] [ContinuousNeg H] {a : H} : Filter.Tendsto Neg.neg (nhdsWithin a (Set.Ici a)) (nhdsWithin (-a) (Set.Iic (-a)))

theorem tendsto_inv_nhdsWithin_Ici {H : Type x} [TopologicalSpace H] [OrderedCommGroup H] [ContinuousInv H] {a : H} : Filter.Tendsto Inv.inv (nhdsWithin a (Set.Ici a)) (nhdsWithin a⁻¹ (Set.Iic a⁻¹))

theorem tendsto_neg_nhdsWithin_Iic {H : Type x} [TopologicalSpace H] [OrderedAddCommGroup H] [ContinuousNeg H] {a : H} : Filter.Tendsto Neg.neg (nhdsWithin a (Set.Iic a)) (nhdsWithin (-a) (Set.Ici (-a)))

theorem tendsto_inv_nhdsWithin_Iic {H : Type x} [TopologicalSpace H] [OrderedCommGroup H] [ContinuousInv H] {a : H} : Filter.Tendsto Inv.inv (nhdsWithin a (Set.Iic a)) (nhdsWithin a⁻¹ (Set.Ici a⁻¹))

theorem tendsto_neg_nhdsWithin_Ici_neg {H : Type x} [TopologicalSpace H] [OrderedAddCommGroup H] [ContinuousNeg H] {a : H} : Filter.Tendsto Neg.neg (nhdsWithin (-a) (Set.Ici (-a))) (nhdsWithin a (Set.Iic a))

theorem tendsto_inv_nhdsWithin_Ici_inv {H : Type x} [TopologicalSpace H] [OrderedCommGroup H] [ContinuousInv H] {a : H} : Filter.Tendsto Inv.inv (nhdsWithin a⁻¹ (Set.Ici a⁻¹)) (nhdsWithin a (Set.Iic a))

theorem tendsto_neg_nhdsWithin_Iic_neg {H : Type x} [TopologicalSpace H] [OrderedAddCommGroup H] [ContinuousNeg H] {a : H} : Filter.Tendsto Neg.neg (nhdsWithin (-a) (Set.Iic (-a))) (nhdsWithin a (Set.Ici a))

theorem tendsto_inv_nhdsWithin_Iic_inv {H : Type x} [TopologicalSpace H] [OrderedCommGroup H] [ContinuousInv H] {a : H} : Filter.Tendsto Inv.inv (nhdsWithin a⁻¹ (Set.Iic a⁻¹)) (nhdsWithin a (Set.Ici a))

instance instTopologicalAddGroupSum {G : Type w} {H : Type x} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [TopologicalSpace H] [AddGroup H] [TopologicalAddGroup H] : TopologicalAddGroup (G × H)

Equations

• ⋯ = ⋯

instance instTopologicalGroupProd {G : Type w} {H : Type x} [TopologicalSpace G] [Group G] [TopologicalGroup G] [TopologicalSpace H] [Group H] [TopologicalGroup H] : TopologicalGroup (G × H)

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} [TopologicalSpace α] [Neg α] [ContinuousNeg α] : ContinuousNeg αᵃᵒᵖ

Equations

• ⋯ = ⋯

instance instContinuousInvMulOpposite {α : Type u} [TopologicalSpace α] [Inv α] [ContinuousInv α] : ContinuousInv αᵐᵒᵖ

Equations

• ⋯ = ⋯

instance instTopologicalAddGroupAddOpposite {α : Type u} [TopologicalSpace α] [AddGroup α] [TopologicalAddGroup α] : TopologicalAddGroup αᵃᵒᵖ

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

Equations

• ⋯ = ⋯

instance instTopologicalGroupMulOpposite {α : Type u} [TopologicalSpace α] [Group α] [TopologicalGroup α] : TopologicalGroup αᵐᵒᵖ

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

Equations

• ⋯ = ⋯

theorem nhds_zero_symm (G : Type w) [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] : Filter.comap Neg.neg (nhds 0) = nhds 0

theorem nhds_one_symm (G : Type w) [TopologicalSpace G] [Group G] [TopologicalGroup G] : Filter.comap Inv.inv (nhds 1) = nhds 1

theorem nhds_zero_symm' (G : Type w) [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] : Filter.map Neg.neg (nhds 0) = nhds 0

theorem nhds_one_symm' (G : Type w) [TopologicalSpace G] [Group G] [TopologicalGroup G] : Filter.map Inv.inv (nhds 1) = nhds 1

theorem neg_mem_nhds_zero (G : Type w) [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {S : Set G} (hS : S ∈ nhds 0) : -S ∈ nhds 0

theorem inv_mem_nhds_one (G : Type w) [TopologicalSpace G] [Group G] [TopologicalGroup G] {S : Set G} (hS : S ∈ nhds 1) : S⁻¹ ∈ nhds 1

theorem Homeomorph.shearAddRight.proof_2 (G : Type u_1) [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] : 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) [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] : Continuous fun (x : G × G) => (x.1, (Equiv.addLeft x.1) x.2)

def Homeomorph.shearAddRight (G : Type w) [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] : G × G ≃ₜ G × G

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

Equations

• Homeomorph.shearAddRight G = { toEquiv := (Equiv.refl G).prodShear Equiv.addLeft, continuous_toFun := ⋯, continuous_invFun := ⋯ }

def Homeomorph.shearMulRight (G : Type w) [TopologicalSpace G] [Group G] [TopologicalGroup G] : G × G ≃ₜ G × G

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

Equations

• Homeomorph.shearMulRight G = { toEquiv := (Equiv.refl G).prodShear Equiv.mulLeft, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.shearAddRight_coe (G : Type w) [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] : ⇑(Homeomorph.shearAddRight G) = fun (z : G × G) => (z.1, z.1 + z.2)

@[simp]

theorem Homeomorph.shearMulRight_coe (G : Type w) [TopologicalSpace G] [Group G] [TopologicalGroup G] : ⇑(Homeomorph.shearMulRight G) = fun (z : G × G) => (z.1, z.1 * z.2)

@[simp]

theorem Homeomorph.shearAddRight_symm_coe (G : Type w) [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] : ⇑(Homeomorph.shearAddRight G).symm = fun (z : G × G) => (z.1, -z.1 + z.2)

@[simp]

theorem Homeomorph.shearMulRight_symm_coe (G : Type w) [TopologicalSpace G] [Group G] [TopologicalGroup G] : ⇑(Homeomorph.shearMulRight G).symm = fun (z : G × G) => (z.1, z.1⁻¹ * z.2)

theorem IsInducing.topologicalAddGroup {G : Type w} {H : Type x} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {F : Type u_1} [AddGroup H] [TopologicalSpace H] [FunLike F H G] [AddMonoidHomClass F H G] (f : F) (hf : IsInducing ⇑f) : TopologicalAddGroup H

theorem IsInducing.topologicalGroup {G : Type w} {H : Type x} [TopologicalSpace G] [Group G] [TopologicalGroup G] {F : Type u_1} [Group H] [TopologicalSpace H] [FunLike F H G] [MonoidHomClass F H G] (f : F) (hf : IsInducing ⇑f) : TopologicalGroup H

@[deprecated IsInducing.topologicalGroup]

theorem Inducing.topologicalGroup {G : Type w} {H : Type x} [TopologicalSpace G] [Group G] [TopologicalGroup G] {F : Type u_1} [Group H] [TopologicalSpace H] [FunLike F H G] [MonoidHomClass F H G] (f : F) (hf : IsInducing ⇑f) : TopologicalGroup H

Alias of IsInducing.topologicalGroup.

theorem topologicalAddGroup_induced {G : Type w} {H : Type x} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {F : Type u_1} [AddGroup H] [FunLike F H G] [AddMonoidHomClass F H G] (f : F) : TopologicalAddGroup H

theorem topologicalGroup_induced {G : Type w} {H : Type x} [TopologicalSpace G] [Group G] [TopologicalGroup G] {F : Type u_1} [Group H] [FunLike F H G] [MonoidHomClass F H G] (f : F) : TopologicalGroup H

instance AddSubgroup.instTopologicalAddGroupSubtypeMem {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (S : AddSubgroup G) : TopologicalAddGroup ↥S

Equations

• ⋯ = ⋯

instance Subgroup.instTopologicalGroupSubtypeMem {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (S : Subgroup G) : TopologicalGroup ↥S

Equations

• ⋯ = ⋯

def AddSubgroup.topologicalClosure {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (s : AddSubgroup G) : AddSubgroup G

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

Equations

• s.topologicalClosure = { carrier := closure ↑s, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

theorem AddSubgroup.topologicalClosure.proof_2 {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (s : AddSubgroup G) : 0 ∈ s.topologicalClosure.carrier

theorem AddSubgroup.topologicalClosure.proof_1 {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (s : AddSubgroup G) : ∀ {a b : G}, a ∈ s.topologicalClosure.carrier → b ∈ s.topologicalClosure.carrier → a + b ∈ s.topologicalClosure.carrier

theorem AddSubgroup.topologicalClosure.proof_3 {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (s : AddSubgroup G) {g : G} (hg : g ∈ { carrier := closure ↑s, add_mem' := ⋯, zero_mem' := ⋯ }.carrier) : -g ∈ { carrier := closure ↑s, add_mem' := ⋯, zero_mem' := ⋯ }.carrier

def Subgroup.topologicalClosure {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (s : Subgroup G) : Subgroup G

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

Equations

• s.topologicalClosure = { carrier := closure ↑s, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

@[simp]

theorem AddSubgroup.topologicalClosure_coe {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {s : AddSubgroup G} : ↑s.topologicalClosure = closure ↑s

@[simp]

theorem Subgroup.topologicalClosure_coe {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {s : Subgroup G} : ↑s.topologicalClosure = closure ↑s

theorem AddSubgroup.le_topologicalClosure {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (s : AddSubgroup G) : s ≤ s.topologicalClosure

theorem Subgroup.le_topologicalClosure {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (s : Subgroup G) : s ≤ s.topologicalClosure

theorem AddSubgroup.isClosed_topologicalClosure {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (s : AddSubgroup G) : IsClosed ↑s.topologicalClosure

theorem Subgroup.isClosed_topologicalClosure {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (s : Subgroup G) : IsClosed ↑s.topologicalClosure

theorem AddSubgroup.topologicalClosure_minimal {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (s : AddSubgroup G) {t : AddSubgroup G} (h : s ≤ t) (ht : IsClosed ↑t) : s.topologicalClosure ≤ t

theorem Subgroup.topologicalClosure_minimal {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (s : Subgroup G) {t : Subgroup G} (h : s ≤ t) (ht : IsClosed ↑t) : s.topologicalClosure ≤ t

theorem DenseRange.topologicalClosure_map_addSubgroup {G : Type w} {H : Type x} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [AddGroup H] [TopologicalSpace H] [TopologicalAddGroup H] {f : G →+ H} (hf : Continuous ⇑f) (hf' : DenseRange ⇑f) {s : AddSubgroup G} (hs : s.topologicalClosure = ⊤) : (AddSubgroup.map f s).topologicalClosure = ⊤

theorem DenseRange.topologicalClosure_map_subgroup {G : Type w} {H : Type x} [TopologicalSpace G] [Group G] [TopologicalGroup G] [Group H] [TopologicalSpace H] [TopologicalGroup H] {f : G →* H} (hf : Continuous ⇑f) (hf' : DenseRange ⇑f) {s : Subgroup G} (hs : s.topologicalClosure = ⊤) : (Subgroup.map f s).topologicalClosure = ⊤

theorem AddSubgroup.is_normal_topologicalClosure {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (N : AddSubgroup G) [N.Normal] : N.topologicalClosure.Normal

The topological closure of a normal additive subgroup is normal.

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

The topological closure of a normal subgroup is normal.

theorem add_mem_connectedComponent_zero {G : Type u_1} [TopologicalSpace G] [AddZeroClass G] [ContinuousAdd G] {g : G} {h : G} (hg : g ∈ connectedComponent 0) (hh : h ∈ connectedComponent 0) : g + h ∈ connectedComponent 0

theorem mul_mem_connectedComponent_one {G : Type u_1} [TopologicalSpace G] [MulOneClass G] [ContinuousMul G] {g : G} {h : G} (hg : g ∈ connectedComponent 1) (hh : h ∈ connectedComponent 1) : g * h ∈ connectedComponent 1

theorem neg_mem_connectedComponent_zero {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {g : G} (hg : g ∈ connectedComponent 0) : -g ∈ connectedComponent 0

theorem inv_mem_connectedComponent_one {G : Type u_1} [TopologicalSpace G] [Group G] [TopologicalGroup G] {g : G} (hg : g ∈ connectedComponent 1) : g⁻¹ ∈ connectedComponent 1

theorem AddSubgroup.connectedComponentOfZero.proof_1 (G : Type u_1) [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] : ∀ {a b : G}, a ∈ connectedComponent 0 → b ∈ connectedComponent 0 → a + b ∈ connectedComponent 0

def AddSubgroup.connectedComponentOfZero (G : Type u_1) [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] : AddSubgroup G

The connected component of 0 is a subgroup of G.

Equations

• AddSubgroup.connectedComponentOfZero G = { carrier := connectedComponent 0, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

theorem AddSubgroup.connectedComponentOfZero.proof_2 (G : Type u_1) [TopologicalSpace G] [AddGroup G] : 0 ∈ connectedComponent 0

def Subgroup.connectedComponentOfOne (G : Type u_1) [TopologicalSpace G] [Group G] [TopologicalGroup G] : Subgroup G

The connected component of 1 is a subgroup of G.

Equations

• Subgroup.connectedComponentOfOne G = { carrier := connectedComponent 1, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

theorem AddSubgroup.addCommGroupTopologicalClosure.proof_1 {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [T2Space G] (s : AddSubgroup G) (hs : ∀ (x y : ↥s), x + y = y + x) (a : ↥s.topologicalClosure) (b : ↥s.topologicalClosure) : a + b = b + a

def AddSubgroup.addCommGroupTopologicalClosure {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [T2Space G] (s : AddSubgroup G) (hs : ∀ (x y : ↥s), x + y = y + x) : AddCommGroup ↥s.topologicalClosure

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

Equations

• s.addCommGroupTopologicalClosure hs = AddCommGroup.mk ⋯

def Subgroup.commGroupTopologicalClosure {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] [T2Space G] (s : Subgroup G) (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 = CommGroup.mk ⋯

theorem AddSubgroup.coe_topologicalClosure_bot (G : Type w) [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] : ↑⊥.topologicalClosure = closure {0}

theorem Subgroup.coe_topologicalClosure_bot (G : Type w) [TopologicalSpace G] [Group G] [TopologicalGroup G] : ↑⊥.topologicalClosure = closure {1}

theorem exists_nhds_half_neg {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {s : Set G} (hs : s ∈ nhds 0) : ∃ V ∈ nhds 0, ∀ v ∈ V, ∀ w ∈ V, v - w ∈ s

theorem exists_nhds_split_inv {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {s : Set G} (hs : s ∈ nhds 1) : ∃ V ∈ nhds 1, ∀ v ∈ V, ∀ w ∈ V, v / w ∈ s

theorem nhds_translation_add_neg {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (x : G) : Filter.comap (fun (x_1 : G) => x_1 + -x) (nhds 0) = nhds x

theorem nhds_translation_mul_inv {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (x : G) : Filter.comap (fun (x_1 : G) => x_1 * x⁻¹) (nhds 1) = nhds x

@[simp]

theorem map_add_left_nhds {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (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} [TopologicalSpace G] [Group G] [TopologicalGroup G] (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} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (x : G) : Filter.map (fun (x_1 : G) => x + x_1) (nhds 0) = nhds x

theorem map_mul_left_nhds_one {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (x : G) : Filter.map (fun (x_1 : G) => x * x_1) (nhds 1) = nhds x

@[simp]

theorem map_add_right_nhds {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (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} [TopologicalSpace G] [Group G] [TopologicalGroup G] (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} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (x : G) : Filter.map (fun (x_1 : G) => x_1 + x) (nhds 0) = nhds x

theorem map_mul_right_nhds_one {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (x : G) : Filter.map (fun (x_1 : G) => x_1 * x) (nhds 1) = nhds x

theorem Filter.HasBasis.nhds_of_zero {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {ι : 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} [TopologicalSpace G] [Group G] [TopologicalGroup G] {ι : 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} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {x : G} {s : Set G} : x ∈ closure s ↔ ∀ U ∈ nhds 0, ∃ y ∈ s, y - x ∈ U

theorem mem_closure_iff_nhds_one {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {x : G} {s : Set G} : x ∈ closure s ↔ ∀ U ∈ nhds 1, ∃ y ∈ s, y / x ∈ U

theorem continuous_of_continuousAt_zero {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {M : Type u_1} {hom : Type u_2} [AddZeroClass M] [TopologicalSpace M] [ContinuousAdd M] [FunLike hom G M] [AddMonoidHomClass hom G M] (f : hom) (hf : ContinuousAt (⇑f) 0) : Continuous ⇑f

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} [TopologicalSpace G] [Group G] [TopologicalGroup G] {M : Type u_1} {hom : Type u_2} [MulOneClass M] [TopologicalSpace M] [ContinuousMul M] [FunLike hom G M] [MonoidHomClass hom G M] (f : hom) (hf : ContinuousAt (⇑f) 1) : Continuous ⇑f

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.

theorem continuous_of_continuousAt_zero₂ {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {H : Type u_1} {M : Type u_2} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] [AddGroup H] [TopologicalSpace H] [TopologicalAddGroup H] (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} [TopologicalSpace G] [Group G] [TopologicalGroup G] {H : Type u_1} {M : Type u_2} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] [Group H] [TopologicalSpace H] [TopologicalGroup H] (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} [AddGroup G] {t : TopologicalSpace G} {t' : TopologicalSpace G} (tg : TopologicalAddGroup G) (tg' : TopologicalAddGroup G) (h : nhds 0 = nhds 0) : t = t'

theorem TopologicalGroup.ext {G : Type u_1} [Group G] {t : TopologicalSpace G} {t' : TopologicalSpace G} (tg : TopologicalGroup G) (tg' : TopologicalGroup G) (h : nhds 1 = nhds 1) : t = t'

theorem TopologicalAddGroup.ext_iff {G : Type u_1} [AddGroup G] {t : TopologicalSpace G} {t' : TopologicalSpace G} (tg : TopologicalAddGroup G) (tg' : TopologicalAddGroup G) : t = t' ↔ nhds 0 = nhds 0

theorem TopologicalGroup.ext_iff {G : Type u_1} [Group G] {t : TopologicalSpace G} {t' : TopologicalSpace G} (tg : TopologicalGroup G) (tg' : TopologicalGroup G) : t = t' ↔ nhds 1 = nhds 1

theorem ContinuousNeg.of_nhds_zero {G : Type u_1} [AddGroup G] [TopologicalSpace G] (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)) : ContinuousNeg G

theorem ContinuousInv.of_nhds_one {G : Type u_1} [Group G] [TopologicalSpace G] (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)) : ContinuousInv G

theorem TopologicalAddGroup.of_nhds_zero' {G : Type u} [AddGroup G] [TopologicalSpace G] (hmul : Filter.Tendsto (Function.uncurry fun (x1 x2 : G) => x1 + x2) (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)) : TopologicalAddGroup G

theorem TopologicalGroup.of_nhds_one' {G : Type u} [Group G] [TopologicalSpace G] (hmul : Filter.Tendsto (Function.uncurry fun (x1 x2 : G) => x1 * x2) (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)) : TopologicalGroup G

theorem TopologicalAddGroup.of_nhds_zero {G : Type u} [AddGroup G] [TopologicalSpace G] (hmul : Filter.Tendsto (Function.uncurry fun (x1 x2 : G) => x1 + x2) (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)) : TopologicalAddGroup G

theorem TopologicalGroup.of_nhds_one {G : Type u} [Group G] [TopologicalSpace G] (hmul : Filter.Tendsto (Function.uncurry fun (x1 x2 : G) => x1 * x2) (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)) : TopologicalGroup G

theorem TopologicalAddGroup.of_comm_of_nhds_zero {G : Type u} [AddCommGroup G] [TopologicalSpace G] (hmul : Filter.Tendsto (Function.uncurry fun (x1 x2 : G) => x1 + x2) (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)) : TopologicalAddGroup G

theorem TopologicalGroup.of_comm_of_nhds_one {G : Type u} [CommGroup G] [TopologicalSpace G] (hmul : Filter.Tendsto (Function.uncurry fun (x1 x2 : G) => x1 * x2) (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)) : TopologicalGroup G

theorem TopologicalAddGroup.exists_antitone_basis_nhds_zero (G : Type w) [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [FirstCountableTopology G] : ∃ (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) [TopologicalSpace G] [Group G] [TopologicalGroup G] [FirstCountableTopology G] : ∃ (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

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

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

• continuous_sub : Continuous fun (p : G × G) => p.1 - p.2

theorem ContinuousSub.continuous_sub {G : Type u_1} : ∀ {inst : TopologicalSpace G} {inst_1 : Sub G} [self : ContinuousSub G], Continuous fun (p : G × G) => p.1 - p.2

class ContinuousDiv (G : Type u_1) [TopologicalSpace G] [Div G] : Prop

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

• continuous_div' : Continuous fun (p : G × G) => p.1 / p.2

theorem ContinuousDiv.continuous_div' {G : Type u_1} : ∀ {inst : TopologicalSpace G} {inst_1 : Div G} [self : ContinuousDiv G], Continuous fun (p : G × G) => p.1 / p.2

@[instance 100]

instance TopologicalAddGroup.to_continuousSub {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] : ContinuousSub G

Equations

• ⋯ = ⋯

@[instance 100]

instance TopologicalGroup.to_continuousDiv {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] : ContinuousDiv G

Equations

• ⋯ = ⋯

theorem Filter.Tendsto.sub {G : Type w} {α : Type u} [TopologicalSpace G] [Sub G] [ContinuousSub G] {f : α → G} {g : α → G} {l : Filter α} {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} [TopologicalSpace G] [Div G] [ContinuousDiv G] {f : α → G} {g : α → G} {l : Filter α} {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} [TopologicalSpace G] [Sub G] [ContinuousSub G] (b : G) {c : G} {f : α → G} {l : Filter α} (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} [TopologicalSpace G] [Div G] [ContinuousDiv G] (b : G) {c : G} {f : α → G} {l : Filter α} (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} [AddCommGroup G] [TopologicalSpace G] [ContinuousSub G] (b : G) {c : G} {f : α → G} {l : Filter α} : 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} [CommGroup G] [TopologicalSpace G] [ContinuousDiv G] (b : G) {c : G} {f : α → G} {l : Filter α} : 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} [TopologicalSpace G] [Sub G] [ContinuousSub G] {c : G} {f : α → G} {l : Filter α} (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} [TopologicalSpace G] [Div G] [ContinuousDiv G] {c : G} {f : α → G} {l : Filter α} (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} [CommGroupWithZero G] [TopologicalSpace G] [ContinuousDiv G] {b : G} (hb : b ≠ 0) {c : G} {f : α → G} {l : Filter α} : 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} [AddCommGroup G] [TopologicalSpace G] [ContinuousSub G] (b : G) {c : G} {f : α → G} {l : Filter α} : 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} [TopologicalSpace G] [Sub G] [ContinuousSub G] [TopologicalSpace α] {f : α → G} {g : α → G} (hf : Continuous f) (hg : Continuous g) : Continuous fun (x : α) => f x - g x

theorem Continuous.div' {G : Type w} {α : Type u} [TopologicalSpace G] [Div G] [ContinuousDiv G] [TopologicalSpace α] {f : α → G} {g : α → G} (hf : Continuous f) (hg : Continuous g) : Continuous fun (x : α) => f x / g x

theorem continuous_sub_left {G : Type w} [TopologicalSpace G] [Sub G] [ContinuousSub G] (a : G) : Continuous fun (x : G) => a - x

theorem continuous_div_left' {G : Type w} [TopologicalSpace G] [Div G] [ContinuousDiv G] (a : G) : Continuous fun (x : G) => a / x

theorem continuous_sub_right {G : Type w} [TopologicalSpace G] [Sub G] [ContinuousSub G] (a : G) : Continuous fun (x : G) => x - a

theorem continuous_div_right' {G : Type w} [TopologicalSpace G] [Div G] [ContinuousDiv G] (a : G) : Continuous fun (x : G) => x / a

theorem ContinuousAt.sub {G : Type w} {α : Type u} [TopologicalSpace G] [Sub G] [ContinuousSub G] [TopologicalSpace α] {f : α → G} {g : α → G} {x : α} (hf : ContinuousAt f x) (hg : ContinuousAt g x) : ContinuousAt (fun (x : α) => f x - g x) x

theorem ContinuousAt.div' {G : Type w} {α : Type u} [TopologicalSpace G] [Div G] [ContinuousDiv G] [TopologicalSpace α] {f : α → G} {g : α → G} {x : α} (hf : ContinuousAt f x) (hg : ContinuousAt g x) : ContinuousAt (fun (x : α) => f x / g x) x

theorem ContinuousWithinAt.sub {G : Type w} {α : Type u} [TopologicalSpace G] [Sub G] [ContinuousSub G] [TopologicalSpace α] {f : α → G} {g : α → G} {s : Set α} {x : α} (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) : ContinuousWithinAt (fun (x : α) => f x - g x) s x

theorem ContinuousWithinAt.div' {G : Type w} {α : Type u} [TopologicalSpace G] [Div G] [ContinuousDiv G] [TopologicalSpace α] {f : α → G} {g : α → G} {s : Set α} {x : α} (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) : ContinuousWithinAt (fun (x : α) => f x / g x) s x

theorem ContinuousOn.sub {G : Type w} {α : Type u} [TopologicalSpace G] [Sub G] [ContinuousSub G] [TopologicalSpace α] {f : α → G} {g : α → G} {s : Set α} (hf : ContinuousOn f s) (hg : ContinuousOn g s) : ContinuousOn (fun (x : α) => f x - g x) s

theorem ContinuousOn.div' {G : Type w} {α : Type u} [TopologicalSpace G] [Div G] [ContinuousDiv G] [TopologicalSpace α] {f : α → G} {g : α → G} {s : Set α} (hf : ContinuousOn f s) (hg : ContinuousOn g s) : ContinuousOn (fun (x : α) => f x / g x) s

theorem Homeomorph.subLeft.proof_1 {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (x : G) : Continuous fun (x_1 : G) => x - x_1

theorem Homeomorph.subLeft.proof_2 {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (x : G) : Continuous fun (x_1 : G) => -x_1 + x

def Homeomorph.subLeft {G : Type w} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (x : G) : G ≃ₜ G

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

Equations

• Homeomorph.subLeft x = { toEquiv := Equiv.subLeft x, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.subLeft_symm_apply {G : Type w} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (x : G) (b : G) : (Homeomorph.subLeft x).symm b = -b + x

@[simp]

theorem Homeomorph.divLeft_symm_apply {G : Type w} [Group G] [TopologicalSpace G] [TopologicalGroup G] (x : G) (b : G) : (Homeomorph.divLeft x).symm b = b⁻¹ * x

@[simp]

theorem Homeomorph.subLeft_apply {G : Type w} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (x : G) (b : G) : (Homeomorph.subLeft x) b = x - b

@[simp]

theorem Homeomorph.divLeft_apply {G : Type w} [Group G] [TopologicalSpace G] [TopologicalGroup G] (x : G) (b : G) : (Homeomorph.divLeft x) b = x / b

def Homeomorph.divLeft {G : Type w} [Group G] [TopologicalSpace G] [TopologicalGroup G] (x : G) : G ≃ₜ G

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

Equations

• Homeomorph.divLeft x = { toEquiv := Equiv.divLeft x, continuous_toFun := ⋯, continuous_invFun := ⋯ }

theorem isOpenMap_sub_left {G : Type w} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (a : G) : IsOpenMap fun (x : G) => a - x

theorem isOpenMap_div_left {G : Type w} [Group G] [TopologicalSpace G] [TopologicalGroup G] (a : G) : IsOpenMap fun (x : G) => a / x

theorem isClosedMap_sub_left {G : Type w} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (a : G) : IsClosedMap fun (x : G) => a - x

theorem isClosedMap_div_left {G : Type w} [Group G] [TopologicalSpace G] [TopologicalGroup G] (a : G) : IsClosedMap fun (x : G) => a / x

theorem Homeomorph.subRight.proof_2 {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (x : G) : Continuous fun (x_1 : G) => id x_1 + x

def Homeomorph.subRight {G : Type w} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (x : G) : G ≃ₜ G

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

Equations

• Homeomorph.subRight x = { toEquiv := Equiv.subRight x, continuous_toFun := ⋯, continuous_invFun := ⋯ }

theorem Homeomorph.subRight.proof_1 {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (x : G) : Continuous fun (x_1 : G) => id x_1 - x

@[simp]

theorem Homeomorph.divRight_apply {G : Type w} [Group G] [TopologicalSpace G] [TopologicalGroup G] (x : G) (b : G) : (Homeomorph.divRight x) b = b / x

@[simp]

theorem Homeomorph.divRight_symm_apply {G : Type w} [Group G] [TopologicalSpace G] [TopologicalGroup G] (x : G) (b : G) : (Homeomorph.divRight x).symm b = b * x

@[simp]

theorem Homeomorph.subRight_apply {G : Type w} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (x : G) (b : G) : (Homeomorph.subRight x) b = b - x

@[simp]

theorem Homeomorph.subRight_symm_apply {G : Type w} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (x : G) (b : G) : (Homeomorph.subRight x).symm b = b + x

def Homeomorph.divRight {G : Type w} [Group G] [TopologicalSpace G] [TopologicalGroup G] (x : G) : G ≃ₜ G

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

Equations

• Homeomorph.divRight x = { toEquiv := Equiv.divRight x, continuous_toFun := ⋯, continuous_invFun := ⋯ }

theorem isOpenMap_sub_right {G : Type w} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (a : G) : IsOpenMap fun (x : G) => x - a

theorem isOpenMap_div_right {G : Type w} [Group G] [TopologicalSpace G] [TopologicalGroup G] (a : G) : IsOpenMap fun (x : G) => x / a

theorem isClosedMap_sub_right {G : Type w} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (a : G) : IsClosedMap fun (x : G) => x - a

theorem isClosedMap_div_right {G : Type w} [Group G] [TopologicalSpace G] [TopologicalGroup G] (a : G) : IsClosedMap fun (x : G) => x / a

theorem tendsto_sub_nhds_zero_iff {G : Type w} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] {α : Type u_1} {l : Filter α} {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} [Group G] [TopologicalSpace G] [TopologicalGroup G] {α : Type u_1} {l : Filter α} {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} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (x : G) : Filter.comap (fun (x_1 : G) => x_1 - x) (nhds 0) = nhds x

theorem nhds_translation_div {G : Type w} [Group G] [TopologicalSpace G] [TopologicalGroup G] (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} [TopologicalSpace β] [AddGroup α] [AddAction α β] [ContinuousConstVAdd α β] {s : Set α} {t : Set β} [TopologicalSpace α] : interior s +ᵥ interior t ⊆ interior (s +ᵥ t)

theorem subset_interior_smul {α : Type u} {β : Type v} [TopologicalSpace β] [Group α] [MulAction α β] [ContinuousConstSMul α β] {s : Set α} {t : Set β} [TopologicalSpace α] : interior s • interior t ⊆ interior (s • t)

theorem IsClosed.vadd_left_of_isCompact {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [AddGroup α] [AddAction α β] [ContinuousNeg α] [ContinuousVAdd α β] {s : Set α} {t : Set β} (ht : IsClosed t) (hs : IsCompact s) : IsClosed (s +ᵥ t)

theorem IsClosed.smul_left_of_isCompact {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [Group α] [MulAction α β] [ContinuousInv α] [ContinuousSMul α β] {s : Set α} {t : Set β} (ht : IsClosed t) (hs : IsCompact s) : IsClosed (s • t)

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} [TopologicalSpace α] [TopologicalSpace β] [AddGroup α] [AddAction α β] [ContinuousNeg α] [ContinuousVAdd α β] [CompactSpace α] : IsClosedMap Quotient.mk'

theorem MulAction.isClosedMap_quotient {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [Group α] [MulAction α β] [ContinuousInv α] [ContinuousSMul α β] [CompactSpace α] : IsClosedMap Quotient.mk'

theorem IsOpen.add_left {α : Type u} [TopologicalSpace α] [AddGroup α] [ContinuousConstVAdd α α] {s : Set α} {t : Set α} : IsOpen t → IsOpen (s + t)

theorem IsOpen.mul_left {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul α α] {s : Set α} {t : Set α} : IsOpen t → IsOpen (s * t)

theorem subset_interior_add_right {α : Type u} [TopologicalSpace α] [AddGroup α] [ContinuousConstVAdd α α] {s : Set α} {t : Set α} : s + interior t ⊆ interior (s + t)

theorem subset_interior_mul_right {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul α α] {s : Set α} {t : Set α} : s * interior t ⊆ interior (s * t)

theorem subset_interior_add {α : Type u} [TopologicalSpace α] [AddGroup α] [ContinuousConstVAdd α α] {s : Set α} {t : Set α} : interior s + interior t ⊆ interior (s + t)

theorem subset_interior_mul {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul α α] {s : Set α} {t : Set α} : interior s * interior t ⊆ interior (s * t)

theorem singleton_add_mem_nhds {α : Type u} [TopologicalSpace α] [AddGroup α] [ContinuousConstVAdd α α] {s : Set α} (a : α) {b : α} (h : s ∈ nhds b) : {a} + s ∈ nhds (a + b)

theorem singleton_mul_mem_nhds {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul α α] {s : Set α} (a : α) {b : α} (h : s ∈ nhds b) : {a} * s ∈ nhds (a * b)

theorem singleton_add_mem_nhds_of_nhds_zero {α : Type u} [TopologicalSpace α] [AddGroup α] [ContinuousConstVAdd α α] {s : Set α} (a : α) (h : s ∈ nhds 0) : {a} + s ∈ nhds a

theorem singleton_mul_mem_nhds_of_nhds_one {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul α α] {s : Set α} (a : α) (h : s ∈ nhds 1) : {a} * s ∈ nhds a

theorem IsOpen.add_right {α : Type u} [TopologicalSpace α] [AddGroup α] [ContinuousConstVAdd αᵃᵒᵖ α] {s : Set α} {t : Set α} (hs : IsOpen s) : IsOpen (s + t)

theorem IsOpen.mul_right {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul αᵐᵒᵖ α] {s : Set α} {t : Set α} (hs : IsOpen s) : IsOpen (s * t)

theorem subset_interior_add_left {α : Type u} [TopologicalSpace α] [AddGroup α] [ContinuousConstVAdd αᵃᵒᵖ α] {s : Set α} {t : Set α} : interior s + t ⊆ interior (s + t)

theorem subset_interior_mul_left {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul αᵐᵒᵖ α] {s : Set α} {t : Set α} : interior s * t ⊆ interior (s * t)

theorem subset_interior_add' {α : Type u} [TopologicalSpace α] [AddGroup α] [ContinuousConstVAdd αᵃᵒᵖ α] {s : Set α} {t : Set α} : interior s + interior t ⊆ interior (s + t)

theorem subset_interior_mul' {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul αᵐᵒᵖ α] {s : Set α} {t : Set α} : interior s * interior t ⊆ interior (s * t)

theorem add_singleton_mem_nhds {α : Type u} [TopologicalSpace α] [AddGroup α] [ContinuousConstVAdd αᵃᵒᵖ α] {s : Set α} (a : α) {b : α} (h : s ∈ nhds b) : s + {a} ∈ nhds (b + a)

theorem mul_singleton_mem_nhds {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul αᵐᵒᵖ α] {s : Set α} (a : α) {b : α} (h : s ∈ nhds b) : s * {a} ∈ nhds (b * a)

theorem add_singleton_mem_nhds_of_nhds_zero {α : Type u} [TopologicalSpace α] [AddGroup α] [ContinuousConstVAdd αᵃᵒᵖ α] {s : Set α} (a : α) (h : s ∈ nhds 0) : s + {a} ∈ nhds a

theorem mul_singleton_mem_nhds_of_nhds_one {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul αᵐᵒᵖ α] {s : Set α} (a : α) (h : s ∈ nhds 1) : s * {a} ∈ nhds a

theorem IsOpen.sub_left {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {s : Set G} {t : Set G} (ht : IsOpen t) : IsOpen (s - t)

theorem IsOpen.div_left {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {s : Set G} {t : Set G} (ht : IsOpen t) : IsOpen (s / t)

theorem IsOpen.sub_right {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {s : Set G} {t : Set G} (hs : IsOpen s) : IsOpen (s - t)

theorem IsOpen.div_right {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {s : Set G} {t : Set G} (hs : IsOpen s) : IsOpen (s / t)

theorem subset_interior_sub_left {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {s : Set G} {t : Set G} : interior s - t ⊆ interior (s - t)

theorem subset_interior_div_left {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {s : Set G} {t : Set G} : interior s / t ⊆ interior (s / t)

theorem subset_interior_sub_right {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {s : Set G} {t : Set G} : s - interior t ⊆ interior (s - t)

theorem subset_interior_div_right {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {s : Set G} {t : Set G} : s / interior t ⊆ interior (s / t)

theorem subset_interior_sub {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {s : Set G} {t : Set G} : interior s - interior t ⊆ interior (s - t)

theorem subset_interior_div {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {s : Set G} {t : Set G} : interior s / interior t ⊆ interior (s / t)

theorem IsOpen.add_closure {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {s : Set G} (hs : IsOpen s) (t : Set G) : s + closure t = s + t

theorem IsOpen.mul_closure {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {s : Set G} (hs : IsOpen s) (t : Set G) : s * closure t = s * t

theorem IsOpen.closure_add {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {t : Set G} (ht : IsOpen t) (s : Set G) : closure s + t = s + t

theorem IsOpen.closure_mul {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {t : Set G} (ht : IsOpen t) (s : Set G) : closure s * t = s * t

theorem IsOpen.sub_closure {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {s : Set G} (hs : IsOpen s) (t : Set G) : s - closure t = s - t

theorem IsOpen.div_closure {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {s : Set G} (hs : IsOpen s) (t : Set G) : s / closure t = s / t

theorem IsOpen.closure_sub {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {t : Set G} (ht : IsOpen t) (s : Set G) : closure s - t = s - t

theorem IsOpen.closure_div {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {t : Set G} (ht : IsOpen t) (s : Set G) : closure s / t = s / t

theorem IsClosed.add_left_of_isCompact {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {s : Set G} {t : Set G} (ht : IsClosed t) (hs : IsCompact s) : IsClosed (s + t)

theorem IsClosed.mul_left_of_isCompact {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {s : Set G} {t : Set G} (ht : IsClosed t) (hs : IsCompact s) : IsClosed (s * t)

theorem IsClosed.add_right_of_isCompact {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {s : Set G} {t : Set G} (ht : IsClosed t) (hs : IsCompact s) : IsClosed (t + s)

theorem IsClosed.mul_right_of_isCompact {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {s : Set G} {t : Set G} (ht : IsClosed t) (hs : IsCompact s) : IsClosed (t * s)

theorem subset_add_closure_zero {G : Type u_1} [AddZeroClass G] [TopologicalSpace G] (s : Set G) : s ⊆ s + closure {0}

theorem subset_mul_closure_one {G : Type u_1} [MulOneClass G] [TopologicalSpace G] (s : Set G) : s ⊆ s * closure {1}

theorem IsCompact.add_closure_zero_eq_closure {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {K : Set G} (hK : IsCompact K) : K + closure {0} = closure K

theorem IsCompact.mul_closure_one_eq_closure {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {K : Set G} (hK : IsCompact K) : K * closure {1} = closure K

theorem IsClosed.add_closure_zero_eq {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {F : Set G} (hF : IsClosed F) : F + closure {0} = F

theorem IsClosed.mul_closure_one_eq {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {F : Set G} (hF : IsClosed F) : F * closure {1} = F

theorem compl_add_closure_zero_eq {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {t : Set G} (ht : t + closure {0} = t) : tᶜ + closure {0} = tᶜ

theorem compl_mul_closure_one_eq {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {t : Set G} (ht : t * closure {1} = t) : tᶜ * closure {1} = tᶜ

theorem compl_add_closure_zero_eq_iff {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {t : Set G} : tᶜ + closure {0} = tᶜ ↔ t + closure {0} = t

theorem compl_mul_closure_one_eq_iff {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {t : Set G} : tᶜ * closure {1} = tᶜ ↔ t * closure {1} = t

theorem IsOpen.add_closure_zero_eq {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {U : Set G} (hU : IsOpen U) : U + closure {0} = U

theorem IsOpen.mul_closure_one_eq {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {U : Set G} (hU : IsOpen U) : U * closure {1} = U

theorem TopologicalAddGroup.t1Space (G : Type w) [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (h : IsClosed {0}) : T1Space G

theorem TopologicalGroup.t1Space (G : Type w) [TopologicalSpace G] [Group G] [ContinuousMul G] (h : IsClosed {1}) : T1Space G

@[instance 100]

instance TopologicalAddGroup.regularSpace (G : Type w) [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] : RegularSpace G

Equations

• ⋯ = ⋯

@[instance 100]

instance TopologicalGroup.regularSpace (G : Type w) [TopologicalSpace G] [Group G] [TopologicalGroup G] : RegularSpace G

Equations

• ⋯ = ⋯

theorem addGroup_inseparable_iff {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {x : G} {y : G} : Inseparable x y ↔ x - y ∈ closure 0

theorem group_inseparable_iff {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {x : G} {y : G} : Inseparable x y ↔ x / y ∈ closure 1

theorem TopologicalAddGroup.t2Space_iff_zero_closed {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] : T2Space G ↔ IsClosed {0}

theorem TopologicalGroup.t2Space_iff_one_closed {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] : T2Space G ↔ IsClosed {1}

theorem TopologicalAddGroup.t2Space_of_zero_sep {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (H : ∀ (x : G), x ≠ 0 → ∃ U ∈ nhds 0, x ∉ U) : T2Space G

theorem TopologicalGroup.t2Space_of_one_sep {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (H : ∀ (x : G), x ≠ 1 → ∃ U ∈ nhds 1, x ∉ U) : T2Space G

theorem exists_closed_nhds_zero_neg_eq_add_subset {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {U : Set G} (hU : U ∈ nhds 0) : ∃ V ∈ nhds 0, IsClosed V ∧ -V = V ∧ V + V ⊆ U

Given a neighborhood U of the identity, one may find a neighborhood V of the identity which is closed, symmetric, and satisfies V + V ⊆ U.

theorem exists_closed_nhds_one_inv_eq_mul_subset {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {U : Set G} (hU : U ∈ nhds 1) : ∃ V ∈ nhds 1, IsClosed V ∧ V⁻¹ = V ∧ V * V ⊆ U

Given a neighborhood U of the identity, one may find a neighborhood V of the identity which is closed, symmetric, and satisfies V * V ⊆ U.

theorem AddSubgroup.properlyDiscontinuousVAdd_of_tendsto_cofinite {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (S : AddSubgroup G) (hS : Filter.Tendsto (⇑S.subtype) Filter.cofinite (Filter.cocompact G)) : ProperlyDiscontinuousVAdd (↥S) G

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} [TopologicalSpace G] [Group G] [TopologicalGroup G] (S : Subgroup G) (hS : Filter.Tendsto (⇑S.subtype) Filter.cofinite (Filter.cocompact G)) : ProperlyDiscontinuousSMul (↥S) G

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} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (S : AddSubgroup G) (hS : Filter.Tendsto (⇑S.subtype) Filter.cofinite (Filter.cocompact G)) : ProperlyDiscontinuousVAdd (↥S.op) G

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} [TopologicalSpace G] [Group G] [TopologicalGroup G] (S : Subgroup G) (hS : Filter.Tendsto (⇑S.subtype) Filter.cofinite (Filter.cocompact G)) : ProperlyDiscontinuousSMul (↥S.op) 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} [TopologicalSpace G] [AddZeroClass G] [ContinuousAdd G] {K : Set G} {U : Set G} (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U) : ∃ 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} [TopologicalSpace G] [MulOneClass G] [ContinuousMul G] {K : Set G} {U : Set G} (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U) : ∃ 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} [TopologicalSpace G] [AddZeroClass G] [ContinuousAdd G] {K : Set G} {U : Set G} (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U) : ∃ 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} [TopologicalSpace G] [MulOneClass G] [ContinuousMul G] {K : Set G} {U : Set G} (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U) : ∃ 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} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {K : Set G} {V : Set G} (hK : IsCompact K) (hV : (interior V).Nonempty) : ∃ (t : Finset G), K ⊆ ⋃ g ∈ t, (fun (x : G) => g + x) ⁻¹' 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} [TopologicalSpace G] [Group G] [TopologicalGroup G] {K : Set G} {V : Set G} (hK : IsCompact K) (hV : (interior V).Nonempty) : ∃ (t : Finset G), K ⊆ ⋃ g ∈ t, (fun (x : G) => g * x) ⁻¹' V

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

@[instance 100]

instance SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [TopologicalSpace.SeparableSpace G] [WeaklyLocallyCompactSpace G] : SigmaCompactSpace G

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

Equations

• ⋯ = ⋯

@[instance 100]

instance SeparableWeaklyLocallyCompactGroup.sigmaCompactSpace {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] [TopologicalSpace.SeparableSpace G] [WeaklyLocallyCompactSpace G] : SigmaCompactSpace G

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

Equations

• ⋯ = ⋯

theorem exists_disjoint_vadd_of_isCompact {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [NoncompactSpace G] {K : Set G} {L : Set G} (hK : IsCompact K) (hL : IsCompact L) : ∃ (g : 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} [TopologicalSpace G] [Group G] [TopologicalGroup G] [NoncompactSpace G] {K : Set G} {L : Set G} (hK : IsCompact K) (hL : IsCompact L) : ∃ (g : 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.

@[deprecated IsCompact.isCompact_isClosed_basis_nhds]

theorem exists_isCompact_isClosed_subset_isCompact_nhds_zero {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {L : Set G} (Lcomp : IsCompact L) (L1 : L ∈ nhds 0) : ∃ (K : Set G), IsCompact K ∧ IsClosed 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.

@[deprecated IsCompact.isCompact_isClosed_basis_nhds]

theorem exists_isCompact_isClosed_subset_isCompact_nhds_one {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {L : Set G} (Lcomp : IsCompact L) (L1 : L ∈ nhds 1) : ∃ (K : Set G), IsCompact K ∧ IsClosed 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 IsCompact.locallyCompactSpace_of_mem_nhds_of_addGroup {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {K : Set G} (hK : IsCompact K) {x : G} (h : K ∈ nhds x) : LocallyCompactSpace G

theorem IsCompact.locallyCompactSpace_of_mem_nhds_of_group {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {K : Set G} (hK : IsCompact K) {x : G} (h : K ∈ nhds x) : LocallyCompactSpace G

If a point in a topological group has a compact neighborhood, then the group is locally compact.

@[deprecated WeaklyLocallyCompactSpace.locallyCompactSpace]

theorem instLocallyCompactSpaceOfWeaklyOfAddGroup {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [WeaklyLocallyCompactSpace G] : LocallyCompactSpace G

@[deprecated WeaklyLocallyCompactSpace.locallyCompactSpace]

theorem instLocallyCompactSpaceOfWeaklyOfGroup {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] [WeaklyLocallyCompactSpace G] : LocallyCompactSpace G

A topological group which is weakly locally compact is automatically locally compact.

theorem eq_zero_or_locallyCompactSpace_of_support_subset_isCompact_of_addGroup {G : Type w} {α : Type u} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [TopologicalSpace α] [Zero α] [T1Space α] {f : G → α} {k : Set G} (hk : IsCompact k) (hf : Function.support f ⊆ k) (h'f : Continuous f) : f = 0 ∨ LocallyCompactSpace G

If a function defined on a topological additive group has a support contained in a compact set, then either the function is trivial or the group is locally compact.

theorem eq_zero_or_locallyCompactSpace_of_support_subset_isCompact_of_group {G : Type w} {α : Type u} [TopologicalSpace G] [Group G] [TopologicalGroup G] [TopologicalSpace α] [Zero α] [T1Space α] {f : G → α} {k : Set G} (hk : IsCompact k) (hf : Function.support f ⊆ k) (h'f : Continuous f) : f = 0 ∨ LocallyCompactSpace G

If a function defined on a topological group has a support contained in a compact set, then either the function is trivial or the group is locally compact.

theorem HasCompactSupport.eq_zero_or_locallyCompactSpace_of_addGroup {G : Type w} {α : Type u} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [TopologicalSpace α] [Zero α] [T1Space α] {f : G → α} (hf : HasCompactSupport f) (h'f : Continuous f) : f = 0 ∨ LocallyCompactSpace G

If a function defined on a topological additive group has compact support, then either the function is trivial or the group is locally compact.

theorem HasCompactSupport.eq_zero_or_locallyCompactSpace_of_group {G : Type w} {α : Type u} [TopologicalSpace G] [Group G] [TopologicalGroup G] [TopologicalSpace α] [Zero α] [T1Space α] {f : G → α} (hf : HasCompactSupport f) (h'f : Continuous f) : f = 0 ∨ LocallyCompactSpace G

If a function defined on a topological group has compact support, then either the function is trivial or the group is locally compact.

@[deprecated isCompact_isClosed_basis_nhds]

theorem local_isCompact_isClosed_nhds_of_addGroup {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [LocallyCompactSpace G] {U : Set G} (hU : U ∈ nhds 0) : ∃ (K : Set G), IsCompact K ∧ IsClosed K ∧ K ⊆ U ∧ 0 ∈ interior K

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.

@[deprecated isCompact_isClosed_basis_nhds]

theorem local_isCompact_isClosed_nhds_of_group {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] [LocallyCompactSpace G] {U : Set G} (hU : U ∈ nhds 1) : ∃ (K : Set G), IsCompact K ∧ IsClosed K ∧ K ⊆ U ∧ 1 ∈ interior K

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.

@[deprecated exists_mem_nhds_isCompact_isClosed]

theorem exists_isCompact_isClosed_nhds_zero (G : Type w) [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [WeaklyLocallyCompactSpace G] : ∃ (K : Set G), IsCompact K ∧ IsClosed K ∧ K ∈ nhds 0

@[deprecated exists_mem_nhds_isCompact_isClosed]

theorem exists_isCompact_isClosed_nhds_one (G : Type w) [TopologicalSpace G] [Group G] [TopologicalGroup G] [WeaklyLocallyCompactSpace G] : ∃ (K : Set G), IsCompact K ∧ IsClosed K ∧ K ∈ nhds 1

theorem nhds_add {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (x : G) (y : G) : nhds (x + y) = nhds x + nhds y

theorem nhds_mul {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (x : G) (y : G) : nhds (x * y) = nhds x * nhds y

def nhdsAddHom {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] : AddHom G (Filter G)

On an additive topological group, 𝓝 : G → Filter G can be promoted to an AddHom.

Equations

• nhdsAddHom = { toFun := nhds, map_add' := ⋯ }

@[simp]

theorem nhdsAddHom_apply {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (x : G) : nhdsAddHom x = nhds x

@[simp]

theorem nhdsMulHom_apply {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (x : G) : nhdsMulHom x = nhds x

def nhdsMulHom {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] : G →ₙ* Filter G

On a topological group, 𝓝 : G → Filter G can be promoted to a MulHom.

Equations

• nhdsMulHom = { toFun := nhds, map_mul' := ⋯ }

instance instTopologicalAddGroupAdditiveOfTopologicalGroup {G : Type u_1} [TopologicalSpace G] [Group G] [TopologicalGroup G] : TopologicalAddGroup (Additive G)

Equations

• ⋯ = ⋯

instance instTopologicalGroupMultiplicativeOfTopologicalAddGroup {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] : TopologicalGroup (Multiplicative G)

Equations

• ⋯ = ⋯

def toAddUnits_homeomorph {G : Type w} [AddGroup G] [TopologicalSpace G] [ContinuousNeg G] : G ≃ₜ AddUnits G

If G is an additive group with topological negation, then it is homeomorphic to its additive units.

Equations

• toAddUnits_homeomorph = { toEquiv := toAddUnits.toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

theorem toAddUnits_homeomorph.proof_1 {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousNeg G] : Continuous toAddUnits.toFun

theorem toAddUnits_homeomorph.proof_2 {G : Type u_1} [AddGroup G] [TopologicalSpace G] : Continuous AddUnits.val

def toUnits_homeomorph {G : Type w} [Group G] [TopologicalSpace G] [ContinuousInv G] : G ≃ₜ Gˣ

If G is a group with topological ⁻¹, then it is homeomorphic to its units.

Equations

• toUnits_homeomorph = { toEquiv := toUnits.toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

theorem AddUnits.isEmbedding_val {G : Type w} [AddGroup G] [TopologicalSpace G] [ContinuousNeg G] : IsEmbedding AddUnits.val

theorem Units.isEmbedding_val {G : Type w} [Group G] [TopologicalSpace G] [ContinuousInv G] : IsEmbedding Units.val

@[deprecated Units.isEmbedding_val]

theorem Units.embedding_val {G : Type w} [Group G] [TopologicalSpace G] [ContinuousInv G] : IsEmbedding Units.val

Alias of Units.isEmbedding_val.

instance AddUnits.instTopologicalAddGroupOfContinuousAdd {α : Type u} [AddMonoid α] [TopologicalSpace α] [ContinuousAdd α] : TopologicalAddGroup (AddUnits α)

Equations

• ⋯ = ⋯

instance Units.instTopologicalGroupOfContinuousMul {α : Type u} [Monoid α] [TopologicalSpace α] [ContinuousMul α] : TopologicalGroup αˣ

Equations

• ⋯ = ⋯

def AddUnits.Homeomorph.sumAddUnits {α : Type u} {β : Type v} [AddMonoid α] [TopologicalSpace α] [AddMonoid β] [TopologicalSpace β] : AddUnits (α × β) ≃ₜ AddUnits α × AddUnits β

The topological group isomorphism between the additive units of a product of two additive monoids, and the product of the additive units of each additive monoid.

Equations

• AddUnits.Homeomorph.sumAddUnits = { toEquiv := AddEquiv.prodAddUnits.toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

theorem AddUnits.Homeomorph.sumAddUnits.proof_2 {α : Type u_1} {β : Type u_2} [AddMonoid α] [TopologicalSpace α] [AddMonoid β] [TopologicalSpace β] : Continuous AddEquiv.prodAddUnits.invFun

theorem AddUnits.Homeomorph.sumAddUnits.proof_1 {α : Type u_1} {β : Type u_2} [AddMonoid α] [TopologicalSpace α] [AddMonoid β] [TopologicalSpace β] : Continuous fun (x : AddUnits (α × β)) => ((AddUnits.map (AddMonoidHom.fst α β)) x, (AddUnits.map (AddMonoidHom.snd α β)) x)

def Units.Homeomorph.prodUnits {α : Type u} {β : Type v} [Monoid α] [TopologicalSpace α] [Monoid β] [TopologicalSpace β] : (α × β)ˣ ≃ₜ αˣ × βˣ

The topological group isomorphism between the units of a product of two monoids, and the product of the units of each monoid.

Equations

• Units.Homeomorph.prodUnits = { toEquiv := MulEquiv.prodUnits.toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

theorem topologicalAddGroup_sInf {G : Type w} [AddGroup G] {ts : Set (TopologicalSpace G)} (h : ∀ t ∈ ts, TopologicalAddGroup G) : TopologicalAddGroup G

theorem topologicalGroup_sInf {G : Type w} [Group G] {ts : Set (TopologicalSpace G)} (h : ∀ t ∈ ts, TopologicalGroup G) : TopologicalGroup G

theorem topologicalAddGroup_iInf {G : Type w} {ι : Sort u_1} [AddGroup G] {ts' : ι → TopologicalSpace G} (h' : ∀ (i : ι), TopologicalAddGroup G) : TopologicalAddGroup G

theorem topologicalGroup_iInf {G : Type w} {ι : Sort u_1} [Group G] {ts' : ι → TopologicalSpace G} (h' : ∀ (i : ι), TopologicalGroup G) : TopologicalGroup G

theorem topologicalAddGroup_inf {G : Type w} [AddGroup G] {t₁ : TopologicalSpace G} {t₂ : TopologicalSpace G} (h₁ : TopologicalAddGroup G) (h₂ : TopologicalAddGroup G) : TopologicalAddGroup G

theorem topologicalGroup_inf {G : Type w} [Group G] {t₁ : TopologicalSpace G} {t₂ : TopologicalSpace G} (h₁ : TopologicalGroup G) (h₂ : TopologicalGroup G) : TopologicalGroup G

Lattice of group topologies

We define a type class GroupTopology α which endows a group α with a topology such that all group operations are continuous.

Group topologies on a fixed group α are ordered, by reverse inclusion. They form a complete lattice, with ⊥ the discrete topology and ⊤ the indiscrete topology.

Any function f : α → β induces coinduced f : TopologicalSpace α → GroupTopology β.

The additive version AddGroupTopology α and corresponding results are provided as well.

structure GroupTopology (α : Type u) [Group α] extends TopologicalSpace , TopologicalGroup : Type u

A group topology on a group α is a topology for which multiplication and inversion are continuous.

structure AddGroupTopology (α : Type u) [AddGroup α] extends TopologicalSpace , TopologicalAddGroup : Type u

An additive group topology on an additive group α is a topology for which addition and negation are continuous.

theorem AddGroupTopology.continuous_add' {α : Type u} [AddGroup α] (g : AddGroupTopology α) : Continuous fun (p : α × α) => p.1 + p.2

A version of the global continuous_add suitable for dot notation.

theorem GroupTopology.continuous_mul' {α : Type u} [Group α] (g : GroupTopology α) : Continuous fun (p : α × α) => p.1 * p.2

A version of the global continuous_mul suitable for dot notation.

theorem AddGroupTopology.continuous_neg' {α : Type u} [AddGroup α] (g : AddGroupTopology α) : Continuous Neg.neg

A version of the global continuous_neg suitable for dot notation.

theorem GroupTopology.continuous_inv' {α : Type u} [Group α] (g : GroupTopology α) : Continuous Inv.inv

A version of the global continuous_inv suitable for dot notation.

theorem AddGroupTopology.toTopologicalSpace_injective {α : Type u} [AddGroup α] : Function.Injective AddGroupTopology.toTopologicalSpace

theorem GroupTopology.toTopologicalSpace_injective {α : Type u} [Group α] : Function.Injective GroupTopology.toTopologicalSpace

theorem AddGroupTopology.ext' {α : Type u} [AddGroup α] {f : AddGroupTopology α} {g : AddGroupTopology α} (h : TopologicalSpace.IsOpen = TopologicalSpace.IsOpen) : f = g

theorem GroupTopology.ext'_iff {α : Type u} [Group α] {f : GroupTopology α} {g : GroupTopology α} : f = g ↔ TopologicalSpace.IsOpen = TopologicalSpace.IsOpen

theorem AddGroupTopology.ext'_iff {α : Type u} [AddGroup α] {f : AddGroupTopology α} {g : AddGroupTopology α} : f = g ↔ TopologicalSpace.IsOpen = TopologicalSpace.IsOpen

theorem GroupTopology.ext' {α : Type u} [Group α] {f : GroupTopology α} {g : GroupTopology α} (h : TopologicalSpace.IsOpen = TopologicalSpace.IsOpen) : f = g

instance AddGroupTopology.instPartialOrder {α : Type u} [AddGroup α] : PartialOrder (AddGroupTopology α)

The ordering on group topologies on the group γ. t ≤ s if every set open in s is also open in t (t is finer than s).

Equations

• AddGroupTopology.instPartialOrder = PartialOrder.lift AddGroupTopology.toTopologicalSpace ⋯

instance GroupTopology.instPartialOrder {α : Type u} [Group α] : PartialOrder (GroupTopology α)

The ordering on group topologies on the group γ. t ≤ s if every set open in s is also open in t (t is finer than s).

Equations

• GroupTopology.instPartialOrder = PartialOrder.lift GroupTopology.toTopologicalSpace ⋯

@[simp]

theorem AddGroupTopology.toTopologicalSpace_le {α : Type u} [AddGroup α] {x : AddGroupTopology α} {y : AddGroupTopology α} : x.toTopologicalSpace ≤ y.toTopologicalSpace ↔ x ≤ y

@[simp]

theorem GroupTopology.toTopologicalSpace_le {α : Type u} [Group α] {x : GroupTopology α} {y : GroupTopology α} : x.toTopologicalSpace ≤ y.toTopologicalSpace ↔ x ≤ y

instance AddGroupTopology.instTop {α : Type u} [AddGroup α] : Top (AddGroupTopology α)

Equations

• AddGroupTopology.instTop = { top := { toTopologicalSpace := ⊤, toTopologicalAddGroup := ⋯ } }

theorem AddGroupTopology.instTop.proof_1 {α : Type u_1} [AddGroup α] : TopologicalAddGroup α

instance GroupTopology.instTop {α : Type u} [Group α] : Top (GroupTopology α)

Equations

• GroupTopology.instTop = { top := { toTopologicalSpace := ⊤, toTopologicalGroup := ⋯ } }

@[simp]

theorem AddGroupTopology.toTopologicalSpace_top {α : Type u} [AddGroup α] : ⊤.toTopologicalSpace = ⊤

@[simp]

theorem GroupTopology.toTopologicalSpace_top {α : Type u} [Group α] : ⊤.toTopologicalSpace = ⊤

instance AddGroupTopology.instBot {α : Type u} [AddGroup α] : Bot (AddGroupTopology α)

Equations

• AddGroupTopology.instBot = { bot := { toTopologicalSpace := ⊥, toTopologicalAddGroup := ⋯ } }

theorem AddGroupTopology.instBot.proof_1 {α : Type u_1} [AddGroup α] : TopologicalAddGroup α

instance GroupTopology.instBot {α : Type u} [Group α] : Bot (GroupTopology α)

Equations

• GroupTopology.instBot = { bot := { toTopologicalSpace := ⊥, toTopologicalGroup := ⋯ } }

@[simp]

theorem AddGroupTopology.toTopologicalSpace_bot {α : Type u} [AddGroup α] : ⊥.toTopologicalSpace = ⊥

@[simp]

theorem GroupTopology.toTopologicalSpace_bot {α : Type u} [Group α] : ⊥.toTopologicalSpace = ⊥

instance AddGroupTopology.instBoundedOrder {α : Type u} [AddGroup α] : BoundedOrder (AddGroupTopology α)

Equations

• AddGroupTopology.instBoundedOrder = BoundedOrder.mk

theorem AddGroupTopology.instBoundedOrder.proof_2 {α : Type u_1} [AddGroup α] (x : AddGroupTopology α) : ⊥ ≤ x.toTopologicalSpace

theorem AddGroupTopology.instBoundedOrder.proof_1 {α : Type u_1} [AddGroup α] (x : AddGroupTopology α) : x.toTopologicalSpace ≤ ⊤

instance GroupTopology.instBoundedOrder {α : Type u} [Group α] : BoundedOrder (GroupTopology α)

Equations

• GroupTopology.instBoundedOrder = BoundedOrder.mk

theorem AddGroupTopology.instInf.proof_1 {α : Type u_1} [AddGroup α] (x : AddGroupTopology α) (y : AddGroupTopology α) : TopologicalAddGroup α

instance AddGroupTopology.instInf {α : Type u} [AddGroup α] : Inf (AddGroupTopology α)

Equations

• AddGroupTopology.instInf = { inf := fun (x y : AddGroupTopology α) => { toTopologicalSpace := x.toTopologicalSpace ⊓ y.toTopologicalSpace, toTopologicalAddGroup := ⋯ } }

instance GroupTopology.instInf {α : Type u} [Group α] : Inf (GroupTopology α)

Equations

• GroupTopology.instInf = { inf := fun (x y : GroupTopology α) => { toTopologicalSpace := x.toTopologicalSpace ⊓ y.toTopologicalSpace, toTopologicalGroup := ⋯ } }

@[simp]

theorem AddGroupTopology.toTopologicalSpace_inf {α : Type u} [AddGroup α] (x : AddGroupTopology α) (y : AddGroupTopology α) : (x ⊓ y).toTopologicalSpace = x.toTopologicalSpace ⊓ y.toTopologicalSpace

@[simp]

theorem GroupTopology.toTopologicalSpace_inf {α : Type u} [Group α] (x : GroupTopology α) (y : GroupTopology α) : (x ⊓ y).toTopologicalSpace = x.toTopologicalSpace ⊓ y.toTopologicalSpace

instance AddGroupTopology.instSemilatticeInf {α : Type u} [AddGroup α] : SemilatticeInf (AddGroupTopology α)

Equations

• AddGroupTopology.instSemilatticeInf = Function.Injective.semilatticeInf AddGroupTopology.toTopologicalSpace ⋯ ⋯

instance GroupTopology.instSemilatticeInf {α : Type u} [Group α] : SemilatticeInf (GroupTopology α)

Equations

• GroupTopology.instSemilatticeInf = Function.Injective.semilatticeInf GroupTopology.toTopologicalSpace ⋯ ⋯

instance AddGroupTopology.instInhabited {α : Type u} [AddGroup α] : Inhabited (AddGroupTopology α)

Equations

• AddGroupTopology.instInhabited = { default := ⊤ }

instance GroupTopology.instInhabited {α : Type u} [Group α] : Inhabited (GroupTopology α)

Equations

• GroupTopology.instInhabited = { default := ⊤ }

theorem AddGroupTopology.instInfSet.proof_1 {α : Type u_1} [AddGroup α] (S : Set (AddGroupTopology α)) : TopologicalAddGroup α

instance AddGroupTopology.instInfSet {α : Type u} [AddGroup α] : InfSet (AddGroupTopology α)

Infimum of a collection of additive group topologies

Equations

• AddGroupTopology.instInfSet = { sInf := fun (S : Set (AddGroupTopology α)) => { toTopologicalSpace := sInf (AddGroupTopology.toTopologicalSpace '' S), toTopologicalAddGroup := ⋯ } }

instance GroupTopology.instInfSet {α : Type u} [Group α] : InfSet (GroupTopology α)

Infimum of a collection of group topologies.

Equations

• GroupTopology.instInfSet = { sInf := fun (S : Set (GroupTopology α)) => { toTopologicalSpace := sInf (GroupTopology.toTopologicalSpace '' S), toTopologicalGroup := ⋯ } }

@[simp]

theorem AddGroupTopology.toTopologicalSpace_sInf {α : Type u} [AddGroup α] (s : Set (AddGroupTopology α)) : (sInf s).toTopologicalSpace = sInf (AddGroupTopology.toTopologicalSpace '' s)

@[simp]

theorem GroupTopology.toTopologicalSpace_sInf {α : Type u} [Group α] (s : Set (GroupTopology α)) : (sInf s).toTopologicalSpace = sInf (GroupTopology.toTopologicalSpace '' s)

@[simp]

theorem AddGroupTopology.toTopologicalSpace_iInf {α : Type u} [AddGroup α] {ι : Sort u_1} (s : ι → AddGroupTopology α) : (⨅ (i : ι), s i).toTopologicalSpace = ⨅ (i : ι), (s i).toTopologicalSpace

@[simp]

theorem GroupTopology.toTopologicalSpace_iInf {α : Type u} [Group α] {ι : Sort u_1} (s : ι → GroupTopology α) : (⨅ (i : ι), s i).toTopologicalSpace = ⨅ (i : ι), (s i).toTopologicalSpace

theorem AddGroupTopology.instCompleteSemilatticeInf.proof_2 {α : Type u_1} [AddGroup α] (S : Set (AddGroupTopology α)) (a : AddGroupTopology α) (hab : ∀ b ∈ S, a ≤ b) : a.toTopologicalSpace ≤ sInf (AddGroupTopology.toTopologicalSpace '' S)

theorem AddGroupTopology.instCompleteSemilatticeInf.proof_1 {α : Type u_1} [AddGroup α] : ∀ (x : Set (AddGroupTopology α)), ∀ a ∈ x, sInf x ≤ a

instance AddGroupTopology.instCompleteSemilatticeInf {α : Type u} [AddGroup α] : CompleteSemilatticeInf (AddGroupTopology α)

Group topologies on γ form a complete lattice, with ⊥ the discrete topology and ⊤ the indiscrete topology.

The infimum of a collection of group topologies is the topology generated by all their open sets (which is a group topology).

The supremum of two group topologies s and t is the infimum of the family of all group topologies contained in the intersection of s and t.

Equations

• AddGroupTopology.instCompleteSemilatticeInf = CompleteSemilatticeInf.mk ⋯ ⋯

instance GroupTopology.instCompleteSemilatticeInf {α : Type u} [Group α] : CompleteSemilatticeInf (GroupTopology α)

Group topologies on γ form a complete lattice, with ⊥ the discrete topology and ⊤ the indiscrete topology.

The infimum of a collection of group topologies is the topology generated by all their open sets (which is a group topology).

The supremum of two group topologies s and t is the infimum of the family of all group topologies contained in the intersection of s and t.

Equations

• GroupTopology.instCompleteSemilatticeInf = CompleteSemilatticeInf.mk ⋯ ⋯

theorem AddGroupTopology.instCompleteLattice.proof_8 {α : Type u_1} [AddGroup α] (s : Set (AddGroupTopology α)) (a : AddGroupTopology α) : (∀ b ∈ s, b ≤ a) → sSup s ≤ a

instance AddGroupTopology.instCompleteLattice {α : Type u} [AddGroup α] : CompleteLattice (AddGroupTopology α)

Equations

• AddGroupTopology.instCompleteLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem AddGroupTopology.instCompleteLattice.proof_1 {α : Type u_1} [AddGroup α] (a : AddGroupTopology α) (b : AddGroupTopology α) : a ≤ a ⊔ b

theorem AddGroupTopology.instCompleteLattice.proof_12 {α : Type u_1} [AddGroup α] (a : AddGroupTopology α) : ⊥ ≤ a

theorem AddGroupTopology.instCompleteLattice.proof_10 {α : Type u_1} [AddGroup α] (s : Set (AddGroupTopology α)) (a : AddGroupTopology α) : (∀ b ∈ s, a ≤ b) → a ≤ sInf s

theorem AddGroupTopology.instCompleteLattice.proof_11 {α : Type u_1} [AddGroup α] (a : AddGroupTopology α) : a ≤ ⊤

theorem AddGroupTopology.instCompleteLattice.proof_3 {α : Type u_1} [AddGroup α] (a : AddGroupTopology α) (b : AddGroupTopology α) (c : AddGroupTopology α) : a ≤ c → b ≤ c → a ⊔ b ≤ c

theorem AddGroupTopology.instCompleteLattice.proof_2 {α : Type u_1} [AddGroup α] (a : AddGroupTopology α) (b : AddGroupTopology α) : b ≤ a ⊔ b

theorem AddGroupTopology.instCompleteLattice.proof_6 {α : Type u_1} [AddGroup α] (a : AddGroupTopology α) (b : AddGroupTopology α) (c : AddGroupTopology α) : a ≤ b → a ≤ c → a ≤ b ⊓ c

theorem AddGroupTopology.instCompleteLattice.proof_9 {α : Type u_1} [AddGroup α] (s : Set (AddGroupTopology α)) (a : AddGroupTopology α) : a ∈ s → sInf s ≤ a

theorem AddGroupTopology.instCompleteLattice.proof_7 {α : Type u_1} [AddGroup α] (s : Set (AddGroupTopology α)) (a : AddGroupTopology α) : a ∈ s → a ≤ sSup s

theorem AddGroupTopology.instCompleteLattice.proof_5 {α : Type u_1} [AddGroup α] (a : AddGroupTopology α) (b : AddGroupTopology α) : a ⊓ b ≤ b

theorem AddGroupTopology.instCompleteLattice.proof_4 {α : Type u_1} [AddGroup α] (a : AddGroupTopology α) (b : AddGroupTopology α) : a ⊓ b ≤ a

instance GroupTopology.instCompleteLattice {α : Type u} [Group α] : CompleteLattice (GroupTopology α)

Equations

• GroupTopology.instCompleteLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

def AddGroupTopology.coinduced {α : Type u_1} {β : Type u_2} [t : TopologicalSpace α] [AddGroup β] (f : α → β) : AddGroupTopology β

Given f : α → β and a topology on α, the coinduced additive group topology on β is the finest topology such that f is continuous and β is a topological additive group.

Equations

• AddGroupTopology.coinduced f = sInf {b : AddGroupTopology β | TopologicalSpace.coinduced f t ≤ b.toTopologicalSpace}

def GroupTopology.coinduced {α : Type u_1} {β : Type u_2} [t : TopologicalSpace α] [Group β] (f : α → β) : GroupTopology β

Given f : α → β and a topology on α, the coinduced group topology on β is the finest topology such that f is continuous and β is a topological group.

Equations

• GroupTopology.coinduced f = sInf {b : GroupTopology β | TopologicalSpace.coinduced f t ≤ b.toTopologicalSpace}

theorem AddGroupTopology.coinduced_continuous {α : Type u_1} {β : Type u_2} [t : TopologicalSpace α] [AddGroup β] (f : α → β) : Continuous f

theorem GroupTopology.coinduced_continuous {α : Type u_1} {β : Type u_2} [t : TopologicalSpace α] [Group β] (f : α → β) : Continuous f