Topological groups

This file defines the following typeclasses:

• IsTopologicalGroup, IsTopologicalAddGroup: 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 IsTopologicalGroup 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 (*).

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 := ⋯ }

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 := ⋯ }

@[simp]

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

@[simp]

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

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

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

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

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

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

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 isClosedMap_mul_left {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] (a : G) : IsClosedMap fun (x : G) => a * x

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

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

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

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 := ⋯ }

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 := ⋯ }

@[simp]

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

@[simp]

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

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

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

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

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

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 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 isClosedMap_mul_right {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] (a : G) : IsClosedMap fun (x : G) => x * a

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

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 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 discreteTopology_of_isOpen_singleton_one {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] (h : IsOpen {1}) : DiscreteTopology G

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

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

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

ContinuousInv and ContinuousNeg

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

instance OrderDual.instContinuousInv {G : Type w} [TopologicalSpace G] [Inv G] [ContinuousInv G] : ContinuousInv Gᵒᵈ

instance OrderDual.instContinuousNeg {G : Type w} [TopologicalSpace G] [Neg G] [ContinuousNeg G] : ContinuousNeg Gᵒᵈ

instance Prod.continuousInv {G : Type w} {H : Type x} [TopologicalSpace G] [Inv G] [ContinuousInv G] [TopologicalSpace H] [Inv H] [ContinuousInv H] : ContinuousInv (G × H)

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

instance Pi.continuousInv {ι : Type u_1} {C : ι → Type u_2} [(i : ι) → TopologicalSpace (C i)] [(i : ι) → Inv (C i)] [∀ (i : ι), ContinuousInv (C i)] : ContinuousInv ((i : ι) → C i)

instance Pi.continuousNeg {ι : Type u_1} {C : ι → Type u_2} [(i : ι) → TopologicalSpace (C i)] [(i : ι) → Neg (C i)] [∀ (i : ι), ContinuousNeg (C i)] : ContinuousNeg ((i : ι) → C i)

instance Pi.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.

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.

@[instance 100]

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

@[instance 100]

instance continuousNeg_of_discreteTopology {H : Type x} [TopologicalSpace H] [Neg H] [DiscreteTopology H] : ContinuousNeg H

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)⁻¹}

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}

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

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

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

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

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 := ⋯ }

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 := ⋯ }

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

@[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 continuous_neg_iff {G : Type w} {α : Type u} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] [TopologicalSpace α] {f : α → G} : Continuous (-f) ↔ Continuous f

@[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 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 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

@[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

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 continuousInv_sInf {G : Type w} [Inv G] {ts : Set (TopologicalSpace G)} (h : ∀ t ∈ ts, ContinuousInv G) : ContinuousInv G

theorem continuousNeg_sInf {G : Type w} [Neg G] {ts : Set (TopologicalSpace G)} (h : ∀ t ∈ ts, 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_iInf {G : Type w} {ι' : Sort u_1} [Neg G] {ts' : ι' → TopologicalSpace G} (h' : ∀ (i : ι'), ContinuousNeg G) : ContinuousNeg G

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

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

theorem Topology.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

theorem Topology.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

@[deprecated Topology.IsInducing.continuousInv (since := "2024-10-28")]

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 : Topology.IsInducing f) (hf_inv : ∀ (x : G), f x⁻¹ = (f x)⁻¹) : ContinuousInv G

Alias of Topology.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.

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

theorem IsTopologicalGroup.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 IsTopologicalAddGroup.continuous_addConj_prod {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.

@[deprecated IsTopologicalAddGroup.continuous_addConj_prod (since := "2025-03-11")]

theorem IsTopologicalAddGroup.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

Alias of IsTopologicalAddGroup.continuous_addConj_prod.

---

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

theorem IsTopologicalGroup.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 IsTopologicalAddGroup.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 IsTopologicalGroup.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.

theorem IsTopologicalAddGroup.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.

instance instIsTopologicalGroupULift {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : IsTopologicalGroup (ULift.{u_1, w} G)

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

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

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

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

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

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

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

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

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

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

theorem Filter.Tendsto.zpow {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {α : Type u_1} {l : Filter α} {f : α → G} {x : G} (hf : Tendsto f l (nhds x)) (z : ℤ) : Tendsto (fun (x : α) => f x ^ z) l (nhds (x ^ z))

theorem Filter.Tendsto.zsmul {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {α : Type u_1} {l : Filter α} {f : α → G} {x : G} (hf : Tendsto f l (nhds x)) (z : ℤ) : Tendsto (fun (x : α) => z • f x) l (nhds (z • x))

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

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

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

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

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

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

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

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

@[deprecated tendsto_neg_nhdsGT (since := "2024-12-22")]

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

Alias of tendsto_neg_nhdsGT.

@[deprecated tendsto_inv_nhdsGT (since := "2024-12-22")]

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

Alias of tendsto_inv_nhdsGT.

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

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

@[deprecated tendsto_neg_nhdsLT (since := "2024-12-22")]

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

Alias of tendsto_neg_nhdsLT.

@[deprecated tendsto_inv_nhdsLT (since := "2024-12-22")]

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

Alias of tendsto_inv_nhdsLT.

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

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

@[deprecated tendsto_neg_nhdsGT_neg (since := "2024-12-22")]

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

Alias of tendsto_neg_nhdsGT_neg.

@[deprecated tendsto_inv_nhdsGT_inv (since := "2024-12-22")]

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

Alias of tendsto_inv_nhdsGT_inv.

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

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

@[deprecated tendsto_neg_nhdsLT_neg (since := "2024-12-22")]

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

Alias of tendsto_neg_nhdsLT_neg.

@[deprecated tendsto_inv_nhdsLT_inv (since := "2024-12-22")]

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

Alias of tendsto_inv_nhdsLT_inv.

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

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

@[deprecated tendsto_neg_nhdsGE (since := "2024-12-22")]

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

Alias of tendsto_neg_nhdsGE.

@[deprecated tendsto_inv_nhdsGE (since := "2024-12-22")]

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

Alias of tendsto_inv_nhdsGE.

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

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

@[deprecated tendsto_neg_nhdsLE (since := "2024-12-22")]

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

Alias of tendsto_neg_nhdsLE.

@[deprecated tendsto_inv_nhdsLE (since := "2024-12-22")]

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

Alias of tendsto_inv_nhdsLE.

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

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

@[deprecated tendsto_neg_nhdsGE_neg (since := "2024-12-22")]

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

Alias of tendsto_neg_nhdsGE_neg.

@[deprecated tendsto_inv_nhdsGE_inv (since := "2024-12-22")]

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

Alias of tendsto_inv_nhdsGE_inv.

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

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

@[deprecated tendsto_neg_nhdsLE_neg (since := "2024-12-22")]

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

Alias of tendsto_neg_nhdsLE_neg.

@[deprecated tendsto_inv_nhdsLE_inv (since := "2024-12-22")]

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

Alias of tendsto_inv_nhdsLE_inv.

instance Prod.instIsTopologicalGroup {G : Type w} {H : Type x} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [TopologicalSpace H] [Group H] [IsTopologicalGroup H] : IsTopologicalGroup (G × H)

instance Prod.instIsTopologicalAddGroup {G : Type w} {H : Type x} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [TopologicalSpace H] [AddGroup H] [IsTopologicalAddGroup H] : IsTopologicalAddGroup (G × H)

instance OrderDual.instIsTopologicalGroup {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : IsTopologicalGroup Gᵒᵈ

instance OrderDual.instIsTopologicalAddGroup {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] : IsTopologicalAddGroup Gᵒᵈ

instance Pi.topologicalGroup {β : Type v} {C : β → Type u_1} [(b : β) → TopologicalSpace (C b)] [(b : β) → Group (C b)] [∀ (b : β), IsTopologicalGroup (C b)] : IsTopologicalGroup ((b : β) → C b)

instance Pi.topologicalAddGroup {β : Type v} {C : β → Type u_1} [(b : β) → TopologicalSpace (C b)] [(b : β) → AddGroup (C b)] [∀ (b : β), IsTopologicalAddGroup (C b)] : IsTopologicalAddGroup ((b : β) → C b)

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

instance instContinuousNegAddOpposite {α : Type u} [TopologicalSpace α] [Neg α] [ContinuousNeg α] : ContinuousNeg αᵃᵒᵖ

instance instIsTopologicalGroupMulOpposite {α : Type u} [TopologicalSpace α] [Group α] [IsTopologicalGroup α] : IsTopologicalGroup αᵐᵒᵖ

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

instance instIsTopologicalAddGroupAddOpposite {α : Type u} [TopologicalSpace α] [AddGroup α] [IsTopologicalAddGroup α] : IsTopologicalAddGroup αᵃᵒᵖ

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

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

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

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

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

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

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

def Homeomorph.shearMulRight (G : Type w) [TopologicalSpace G] [Group G] [IsTopologicalGroup 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 := ⋯ }

def Homeomorph.shearAddRight (G : Type w) [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup 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 := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[deprecated Topology.IsInducing.topologicalGroup (since := "2024-10-28")]

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

Alias of Topology.IsInducing.topologicalGroup.

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

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

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

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

def Subgroup.topologicalClosure {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup 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' := ⋯ }

def AddSubgroup.topologicalClosure {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup 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' := ⋯ }

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

The topological closure of a normal subgroup is normal.

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

The topological closure of a normal additive subgroup is normal.

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

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

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

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

def Subgroup.connectedComponentOfOne (G : Type u_1) [TopologicalSpace G] [Group G] [IsTopologicalGroup 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' := ⋯ }

def AddSubgroup.connectedComponentOfZero (G : Type u_1) [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup 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' := ⋯ }

@[reducible, inline]

abbrev Subgroup.commGroupTopologicalClosure {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup 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.

See note [reducible non-instances].

Equations

• s.commGroupTopologicalClosure hs = { toGroup := s.topologicalClosure.toGroup, mul_comm := ⋯ }

@[reducible, inline]

abbrev AddSubgroup.addCommGroupTopologicalClosure {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup 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.

See note [reducible non-instances].

Equations

• s.addCommGroupTopologicalClosure hs = { toAddGroup := s.topologicalClosure.toAddGroup, add_comm := ⋯ }

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

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

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

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

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

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

@[simp]

theorem map_mul_left_nhds {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] (x y : G) : Filter.map (fun (x_1 : G) => x * x_1) (nhds y) = nhds (x * y)

@[simp]

theorem map_add_left_nhds {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (x y : G) : Filter.map (fun (x_1 : G) => x + x_1) (nhds y) = nhds (x + y)

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

theorem map_add_left_nhds_zero {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (x : G) : Filter.map (fun (x_1 : G) => x + x_1) (nhds 0) = nhds x

@[simp]

theorem map_mul_right_nhds {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] (x y : G) : Filter.map (fun (x_1 : G) => x_1 * x) (nhds y) = nhds (y * x)

@[simp]

theorem map_add_right_nhds {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (x y : G) : Filter.map (fun (x_1 : G) => x_1 + x) (nhds y) = nhds (y + x)

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

theorem map_add_right_nhds_zero {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (x : G) : Filter.map (fun (x_1 : G) => x_1 + x) (nhds 0) = nhds x

theorem Filter.HasBasis.nhds_of_one {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup 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 Filter.HasBasis.nhds_of_zero {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup 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 mem_closure_iff_nhds_one {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {x : G} {s : Set G} : x ∈ closure s ↔ ∀ U ∈ nhds 1, ∃ y ∈ s, y / x ∈ U

theorem mem_closure_iff_nhds_zero {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {x : G} {s : Set G} : x ∈ closure s ↔ ∀ U ∈ nhds 0, ∃ y ∈ s, y - x ∈ U

theorem continuous_of_continuousAt_one {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup 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] [IsTopologicalAddGroup 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] [IsTopologicalGroup G] {H : Type u_1} {M : Type u_2} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] [Group H] [TopologicalSpace H] [IsTopologicalGroup 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 continuous_of_continuousAt_zero₂ {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {H : Type u_1} {M : Type u_2} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] [AddGroup H] [TopologicalSpace H] [IsTopologicalAddGroup 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 IsTopologicalGroup.isInducing_iff_nhds_one {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {H : Type u_1} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {F : Type u_2} [FunLike F G H] [MonoidHomClass F G H] {f : F} : Topology.IsInducing ⇑f ↔ nhds 1 = Filter.comap (⇑f) (nhds 1)

theorem IsTopologicalAddGroup.isInducing_iff_nhds_zero {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {H : Type u_1} [AddGroup H] [TopologicalSpace H] [IsTopologicalAddGroup H] {F : Type u_2} [FunLike F G H] [AddMonoidHomClass F G H] {f : F} : Topology.IsInducing ⇑f ↔ nhds 0 = Filter.comap (⇑f) (nhds 0)

theorem TopologicalGroup.isOpenMap_iff_nhds_one {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {H : Type u_1} [Monoid H] [TopologicalSpace H] [ContinuousConstSMul H H] {F : Type u_2} [FunLike F G H] [MonoidHomClass F G H] {f : F} : IsOpenMap ⇑f ↔ nhds 1 ≤ Filter.map (⇑f) (nhds 1)

theorem TopologicalGroup.isOpenMap_iff_nhds_zero {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {H : Type u_1} [AddMonoid H] [TopologicalSpace H] [ContinuousConstVAdd H H] {F : Type u_2} [FunLike F G H] [AddMonoidHomClass F G H] {f : F} : IsOpenMap ⇑f ↔ nhds 0 ≤ Filter.map (⇑f) (nhds 0)

theorem MonoidHom.isOpenQuotientMap_of_isQuotientMap {A : Type u_1} [Group A] [TopologicalSpace A] [ContinuousMul A] {B : Type u_2} [Group B] [TopologicalSpace B] {F : Type u_3} [FunLike F A B] [MonoidHomClass F A B] {φ : F} (hφ : Topology.IsQuotientMap ⇑φ) : IsOpenQuotientMap ⇑φ

Let A and B be topological groups, and let φ : A → B be a continuous surjective group homomorphism. Assume furthermore that φ is a quotient map (i.e., V ⊆ B is open iff φ⁻¹ V is open). Then φ is an open quotient map, and in particular an open map.

theorem AddMonoidHom.isOpenQuotientMap_of_isQuotientMap {A : Type u_1} [AddGroup A] [TopologicalSpace A] [ContinuousAdd A] {B : Type u_2} [AddGroup B] [TopologicalSpace B] {F : Type u_3} [FunLike F A B] [AddMonoidHomClass F A B] {φ : F} (hφ : Topology.IsQuotientMap ⇑φ) : IsOpenQuotientMap ⇑φ

Let A and B be topological additive groups, and let φ : A → B be a continuous surjective additive group homomorphism. Assume furthermore that φ is a quotient map (i.e., V ⊆ B is open iff φ⁻¹ V is open). Then φ is an open quotient map, and in particular an open map.

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

theorem IsTopologicalAddGroup.ext {G : Type u_1} [AddGroup G] {t t' : TopologicalSpace G} (tg : IsTopologicalAddGroup G) (tg' : IsTopologicalAddGroup G) (h : nhds 0 = nhds 0) : t = t'

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

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

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 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 IsTopologicalGroup.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)) : IsTopologicalGroup G

theorem IsTopologicalAddGroup.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)) : IsTopologicalAddGroup G

theorem IsTopologicalGroup.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)) : IsTopologicalGroup G

theorem IsTopologicalAddGroup.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)) : IsTopologicalAddGroup G

theorem IsTopologicalGroup.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)) : IsTopologicalGroup G

theorem IsTopologicalAddGroup.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)) : IsTopologicalAddGroup G

theorem IsTopologicalGroup.exists_antitone_basis_nhds_one (G : Type w) [TopologicalSpace G] [Group G] [IsTopologicalGroup 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

theorem IsTopologicalAddGroup.exists_antitone_basis_nhds_zero (G : Type w) [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup 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 Filter.Tendsto.const_div' {G : Type w} {α : Type u} [TopologicalSpace G] [Div G] [ContinuousDiv G] (b : G) {c : G} {f : α → G} {l : Filter α} (h : Tendsto f l (nhds c)) : Tendsto (fun (k : α) => b / f k) l (nhds (b / c))

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 : Tendsto f l (nhds c)) : Tendsto (fun (k : α) => b - f k) l (nhds (b - 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 α} : Tendsto (fun (k : α) => b / f k) l (nhds (b / c)) ↔ Tendsto f l (nhds 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 α} : Tendsto (fun (k : α) => b - f k) l (nhds (b - c)) ↔ Tendsto f l (nhds c)

theorem Filter.Tendsto.div_const' {G : Type w} {α : Type u} [TopologicalSpace G] [Div G] [ContinuousDiv G] {c : G} {f : α → G} {l : Filter α} (h : Tendsto f l (nhds c)) (b : G) : Tendsto (fun (x : α) => f x / b) l (nhds (c / b))

theorem Filter.Tendsto.sub_const {G : Type w} {α : Type u} [TopologicalSpace G] [Sub G] [ContinuousSub G] {c : G} {f : α → G} {l : Filter α} (h : Tendsto f l (nhds c)) (b : G) : 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 α} : Tendsto (fun (x : α) => f x / b) l (nhds (c / b)) ↔ 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 α} : Tendsto (fun (x : α) => f x - b) l (nhds (c - b)) ↔ Tendsto f l (nhds c)

theorem continuous_div_left' {G : Type w} [TopologicalSpace G] [Div G] [ContinuousDiv G] (a : G) : Continuous fun (x : G) => a / 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_right' {G : Type w} [TopologicalSpace G] [Div G] [ContinuousDiv G] (a : G) : Continuous fun (x : G) => x / a

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

def Homeomorph.divLeft {G : Type w} [Group G] [TopologicalSpace G] [IsTopologicalGroup 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 := ⋯ }

def Homeomorph.subLeft {G : Type w} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup 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_apply {G : Type w} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (x b : G) : (subLeft x) b = x - b

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

def Homeomorph.divRight {G : Type w} [Group G] [TopologicalSpace G] [IsTopologicalGroup 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 := ⋯ }

def Homeomorph.subRight {G : Type w} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup 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 := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

theorem tendsto_div_nhds_one_iff {G : Type w} [Group G] [TopologicalSpace G] [IsTopologicalGroup 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 tendsto_sub_nhds_zero_iff {G : Type w} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup 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 nhds_translation_div {G : Type w} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (x : G) : Filter.comap (fun (x_1 : G) => x_1 / x) (nhds 1) = nhds x

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

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

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

theorem Subgroup.properlyDiscontinuousSMul_of_tendsto_cofinite {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup 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_of_tendsto_cofinite {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup 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_opposite_of_tendsto_cofinite {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup 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.

theorem AddSubgroup.properlyDiscontinuousVAdd_opposite_of_tendsto_cofinite {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup 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.

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

theorem compact_open_separated_mul_right {G : Type w} [TopologicalSpace G] [MulOneClass G] [ContinuousMul G] {K 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_right {G : Type w} [TopologicalSpace G] [AddZeroClass G] [ContinuousAdd G] {K 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_left {G : Type w} [TopologicalSpace G] [MulOneClass G] [ContinuousMul G] {K 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_open_separated_add_left {G : Type w} [TopologicalSpace G] [AddZeroClass G] [ContinuousAdd G] {K 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_covered_by_mul_left_translates {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {K 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.

theorem compact_covered_by_add_left_translates {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {K 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.

@[instance 100]

instance SeparableWeaklyLocallyCompactGroup.sigmaCompactSpace {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup 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.

@[instance 100]

instance SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup 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.

theorem exists_disjoint_smul_of_isCompact {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [NoncompactSpace G] {K 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.

theorem exists_disjoint_vadd_of_isCompact {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [NoncompactSpace G] {K 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 nhds_mul {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] (x y : G) : nhds (x * y) = nhds x * nhds y

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

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

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

Equations

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

def nhdsAddHom {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] : 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 nhdsMulHom_apply {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] (x : G) : nhdsMulHom x = nhds x

@[simp]

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

instance instIsTopologicalAddGroupAdditiveOfIsTopologicalGroup {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : IsTopologicalAddGroup (Additive G)

instance instIsTopologicalGroupMultiplicativeOfIsTopologicalAddGroup {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] : IsTopologicalGroup (Multiplicative G)

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 := ⋯ }

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 Units.isEmbedding_val {G : Type w} [Group G] [TopologicalSpace G] [ContinuousInv G] : Topology.IsEmbedding val

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

@[deprecated Units.isEmbedding_val (since := "2024-10-26")]

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

Alias of Units.isEmbedding_val.

theorem Continuous.of_coeHom_comp {G : Type w} {H : Type x} [Group G] [Monoid H] [TopologicalSpace G] [TopologicalSpace H] [ContinuousInv G] {f : G →* Hˣ} (hf : Continuous ⇑((Units.coeHom H).comp f)) : Continuous ⇑f

instance Units.instIsTopologicalGroupOfContinuousMul {α : Type u} [Monoid α] [TopologicalSpace α] [ContinuousMul α] : IsTopologicalGroup αˣ

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

def 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

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

def Homeomorph.prodAddUnits {α : 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

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

@[deprecated Homeomorph.prodAddUnits (since := "2025-02-21")]

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

Alias of Homeomorph.prodAddUnits.

---

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

• @Units.Homeomorph.sumAddUnits = @Homeomorph.prodAddUnits

@[deprecated Homeomorph.prodUnits (since := "2025-02-21")]

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

Alias of Homeomorph.prodUnits.

---

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 = @Homeomorph.prodUnits

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

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

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

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

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

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