Definitions about topological groups

In this file we define mixin classes ContinuousInv, IsTopologicalGroup, and ContinuousDiv, as well as their additive versions.

These classes say that the corresponding operations are continuous:

• ContinuousInv G says that (·⁻¹) is continuous on G;
• IsTopologicalGroup G says that (· * ·) is continuous on G × G and (·⁻¹) is continuous on G;
• ContinuousDiv G says that (· / ·) is continuous on G.

For groups, ContinuousDiv G is equivalent to IsTopologicalGroup G, but we use the additive version ContinuousSub for types like NNReal, where subtraction is not given by a - b = a + (-b).

We also provide convenience dot notation lemmas like ContinuousAt.neg.

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

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 Filter.Tendsto.inv {G : Type u_1} {α : Type u_2} [TopologicalSpace G] [Inv G] [ContinuousInv G] {f : α → G} {l : Filter α} {y : G} (h : Tendsto f l (nhds y)) : 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 topological groups with zero (including topological fields) assuming additionally that the limit is nonzero, use Filter.Tendsto.inv₀.

theorem Filter.Tendsto.neg {G : Type u_1} {α : Type u_2} [TopologicalSpace G] [Neg G] [ContinuousNeg G] {f : α → G} {l : Filter α} {y : G} (h : Tendsto f l (nhds y)) : 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 Continuous.inv {G : Type u_1} {X : Type u_3} [TopologicalSpace X] [TopologicalSpace G] [Inv G] [ContinuousInv G] {f : X → G} (hf : Continuous f) : Continuous fun (x : X) => (f x)⁻¹

theorem Continuous.neg {G : Type u_1} {X : Type u_3} [TopologicalSpace X] [TopologicalSpace G] [Neg G] [ContinuousNeg G] {f : X → G} (hf : Continuous f) : Continuous fun (x : X) => -f x

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

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

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

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

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

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

class IsTopologicalAddGroup (G : Type u) [TopologicalSpace G] [AddGroup G] extends ContinuousAdd G, ContinuousNeg G : Prop

A topological (additive) group is a group in which the addition and negation 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 IsUniformAddGroup using IsTopologicalAddGroup.toUniformSpace and isUniformAddGroup_of_addCommGroup.

• continuous_add : Continuous fun (p : G × G) => p.1 + p.2
• continuous_neg : Continuous fun (a : G) => -a

@[deprecated IsTopologicalAddGroup (since := "2025-02-14")]

def TopologicalAddGroup (G : Type u) [TopologicalSpace G] [AddGroup G] : Prop

Alias of IsTopologicalAddGroup.

---

A topological (additive) group is a group in which the addition and negation 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 IsUniformAddGroup using IsTopologicalAddGroup.toUniformSpace and isUniformAddGroup_of_addCommGroup.

Equations

• TopologicalAddGroup = IsTopologicalAddGroup

class IsTopologicalGroup (G : Type u_4) [TopologicalSpace G] [Group G] extends ContinuousMul G, ContinuousInv G : 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 IsUniformGroup using IsTopologicalGroup.toUniformSpace and isUniformGroup_of_commGroup.

• continuous_mul : Continuous fun (p : G × G) => p.1 * p.2
• continuous_inv : Continuous fun (a : G) => a⁻¹

@[deprecated IsTopologicalGroup (since := "2025-02-14")]

def TopologicalGroup (G : Type u_4) [TopologicalSpace G] [Group G] : Prop

Alias of IsTopologicalGroup.

---

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 IsUniformGroup using IsTopologicalGroup.toUniformSpace and isUniformGroup_of_commGroup.

Equations

• TopologicalGroup = IsTopologicalGroup

class ContinuousSub (G : Type u_4) [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

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

@[instance 100]

instance IsTopologicalGroup.to_continuousDiv {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : ContinuousDiv G

@[instance 100]

instance IsTopologicalAddGroup.to_continuousSub {G : Type u} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] : ContinuousSub G

theorem Filter.Tendsto.div' {G : Type u_1} {α : Type u_2} [TopologicalSpace G] [Div G] [ContinuousDiv G] {f g : α → G} {l : Filter α} {a b : G} (hf : Tendsto f l (nhds a)) (hg : Tendsto g l (nhds b)) : Tendsto (fun (x : α) => f x / g x) l (nhds (a / b))

theorem Filter.Tendsto.sub {G : Type u_1} {α : Type u_2} [TopologicalSpace G] [Sub G] [ContinuousSub G] {f g : α → G} {l : Filter α} {a b : G} (hf : Tendsto f l (nhds a)) (hg : Tendsto g l (nhds b)) : Tendsto (fun (x : α) => f x - g x) l (nhds (a - b))

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

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

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

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

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

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

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

theorem Continuous.sub {G : Type u_1} {X : Type u_3} [TopologicalSpace X] [TopologicalSpace G] [Sub G] [ContinuousSub G] {f g : X → G} (hf : Continuous f) (hg : Continuous g) : Continuous fun (x : X) => f x - g x