Uniform structure on topological groups

Given a topological group G, one can naturally build two uniform structures (the "left" and "right" ones) on G inducing its topology. This file defines typeclasses for groups equipped with either of these uniform strucures, as well as a separate typeclass for the (very common) case where the given uniform structure coincides with both the left and right uniform structures.

Main declarations

• IsRightUniformGroup and IsRightUniformAddGroup: Multiplicative and additive topological groups endowed with the associated right uniform structure. This means that two points x and y are close precisely when y * x⁻¹ is close to 1 / y + (-x) close to 0.
• IsLeftUniformGroup and IsLeftUniformAddGroup: Multiplicative and additive topological groups endowed with the associated left uniform structure. This means that two points x and y are close precisely when x⁻¹ * y is close to 1 / (-x) + y close to 0.
• IsUniformGroup and IsUniformAddGroup: Multiplicative and additive uniform groups, i.e., groups with uniformly continuous (*) and (⁻¹) / (+) and (-). This corresponds to the conjuction of the two conditions above, although this result is not in Mathlib yet.

Main results

• IsTopologicalAddGroup.rightUniformSpace and comm_topologicalAddGroup_is_uniform can be used to construct a canonical uniformity for a topological additive group.

See Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean for further results.

Implementation Notes

Since the most frequent use case is G being a commutative additive groups, Mathlib originally did essentially all the theory under the assumption IsUniformGroup G. For this reason, you may find results stated under this assumption even though they may hold under either IsRightUniformGroup G or IsLeftUniformGroup G.

class IsRightUniformAddGroup (G : Type u_7) [UniformSpace G] [AddGroup G] extends IsTopologicalAddGroup G : Prop

A right-uniform additive group is a topological additive group endowed with the associated right uniform structure: the uniformity filter 𝓤 G is the inverse image of 𝓝 0 by the map (x, y) ↦ y + (-x).

In other words, we declare that two points x and y are infinitely close precisely when y + (-x) is infinitely close to 0.

• continuous_add : Continuous fun (p : G × G) => p.1 + p.2
• continuous_neg : Continuous fun (a : G) => -a
• uniformity_eq : uniformity G = Filter.comap (fun (x : G × G) => x.2 + -x.1) (nhds 0)

class IsRightUniformGroup (G : Type u_7) [UniformSpace G] [Group G] extends IsTopologicalGroup G : Prop

A right-uniform group is a topological group endowed with the associated right uniform structure: the uniformity filter 𝓤 G is the inverse image of 𝓝 1 by the map (x, y) ↦ y * x⁻¹.

In other words, we declare that two points x and y are infinitely close precisely when y * x⁻¹ is infinitely close to 1.

• continuous_mul : Continuous fun (p : G × G) => p.1 * p.2
• continuous_inv : Continuous fun (a : G) => a⁻¹
• uniformity_eq : uniformity G = Filter.comap (fun (x : G × G) => x.2 * x.1⁻¹) (nhds 1)

class IsLeftUniformAddGroup (G : Type u_7) [UniformSpace G] [AddGroup G] extends IsTopologicalAddGroup G : Prop

A left-uniform additive group is a topological additive group endowed with the associated left uniform structure: the uniformity filter 𝓤 G is the inverse image of 𝓝 0 by the map (x, y) ↦ (-x) + y.

In other words, we declare that two points x and y are infinitely close precisely when (-x) + y is infinitely close to 0.

• continuous_add : Continuous fun (p : G × G) => p.1 + p.2
• continuous_neg : Continuous fun (a : G) => -a
• uniformity_eq : uniformity G = Filter.comap (fun (x : G × G) => -x.1 + x.2) (nhds 0)

class IsLeftUniformGroup (G : Type u_7) [UniformSpace G] [Group G] extends IsTopologicalGroup G : Prop

A left-uniform group is a topological group endowed with the associated left uniform structure: the uniformity filter 𝓤 G is the inverse image of 𝓝 1 by the map (x, y) ↦ x⁻¹ * y.

In other words, we declare that two points x and y are infinitely close precisely when x⁻¹ * y is infinitely close to 1.

• continuous_mul : Continuous fun (p : G × G) => p.1 * p.2
• continuous_inv : Continuous fun (a : G) => a⁻¹
• uniformity_eq : uniformity G = Filter.comap (fun (x : G × G) => x.1⁻¹ * x.2) (nhds 1)

theorem uniformity_eq_comap_mul_inv_nhds_one (Gᵣ : Type u_3) [UniformSpace Gᵣ] [Group Gᵣ] [IsRightUniformGroup Gᵣ] : uniformity Gᵣ = Filter.comap (fun (x : Gᵣ × Gᵣ) => x.2 * x.1⁻¹) (nhds 1)

theorem uniformity_eq_comap_add_neg_nhds_zero (Gᵣ : Type u_3) [UniformSpace Gᵣ] [AddGroup Gᵣ] [IsRightUniformAddGroup Gᵣ] : uniformity Gᵣ = Filter.comap (fun (x : Gᵣ × Gᵣ) => x.2 + -x.1) (nhds 0)

theorem uniformity_eq_comap_inv_mul_nhds_one (Gₗ : Type u_2) [UniformSpace Gₗ] [Group Gₗ] [IsLeftUniformGroup Gₗ] : uniformity Gₗ = Filter.comap (fun (x : Gₗ × Gₗ) => x.1⁻¹ * x.2) (nhds 1)

theorem uniformity_eq_comap_neg_add_nhds_zero (Gₗ : Type u_2) [UniformSpace Gₗ] [AddGroup Gₗ] [IsLeftUniformAddGroup Gₗ] : uniformity Gₗ = Filter.comap (fun (x : Gₗ × Gₗ) => -x.1 + x.2) (nhds 0)

theorem uniformity_eq_comap_mul_inv_nhds_one_swapped (Gᵣ : Type u_3) [UniformSpace Gᵣ] [Group Gᵣ] [IsRightUniformGroup Gᵣ] : uniformity Gᵣ = Filter.comap (fun (x : Gᵣ × Gᵣ) => x.1 * x.2⁻¹) (nhds 1)

theorem uniformity_eq_comap_add_neg_nhds_zero_swapped (Gᵣ : Type u_3) [UniformSpace Gᵣ] [AddGroup Gᵣ] [IsRightUniformAddGroup Gᵣ] : uniformity Gᵣ = Filter.comap (fun (x : Gᵣ × Gᵣ) => x.1 + -x.2) (nhds 0)

theorem uniformity_eq_comap_inv_mul_nhds_one_swapped (Gₗ : Type u_2) [UniformSpace Gₗ] [Group Gₗ] [IsLeftUniformGroup Gₗ] : uniformity Gₗ = Filter.comap (fun (x : Gₗ × Gₗ) => x.2⁻¹ * x.1) (nhds 1)

theorem uniformity_eq_comap_neg_add_nhds_zero_swapped (Gₗ : Type u_2) [UniformSpace Gₗ] [AddGroup Gₗ] [IsLeftUniformAddGroup Gₗ] : uniformity Gₗ = Filter.comap (fun (x : Gₗ × Gₗ) => -x.2 + x.1) (nhds 0)

theorem uniformity_eq_comap_nhds_one (Gᵣ : Type u_3) [UniformSpace Gᵣ] [Group Gᵣ] [IsRightUniformGroup Gᵣ] : uniformity Gᵣ = Filter.comap (fun (x : Gᵣ × Gᵣ) => x.2 / x.1) (nhds 1)

theorem uniformity_eq_comap_nhds_zero (Gᵣ : Type u_3) [UniformSpace Gᵣ] [AddGroup Gᵣ] [IsRightUniformAddGroup Gᵣ] : uniformity Gᵣ = Filter.comap (fun (x : Gᵣ × Gᵣ) => x.2 - x.1) (nhds 0)

theorem uniformity_eq_comap_nhds_one_swapped (Gᵣ : Type u_3) [UniformSpace Gᵣ] [Group Gᵣ] [IsRightUniformGroup Gᵣ] : uniformity Gᵣ = Filter.comap (fun (x : Gᵣ × Gᵣ) => x.1 / x.2) (nhds 1)

theorem uniformity_eq_comap_nhds_zero_swapped (Gᵣ : Type u_3) [UniformSpace Gᵣ] [AddGroup Gᵣ] [IsRightUniformAddGroup Gᵣ] : uniformity Gᵣ = Filter.comap (fun (x : Gᵣ × Gᵣ) => x.1 - x.2) (nhds 0)

class IsUniformGroup (α : Type u_3) [UniformSpace α] [Group α] : Prop

A uniform group is a group in which multiplication and inversion are uniformly continuous.

IsUniformGroup G is equivalent to the fact that G is a topological group, and the uniformity coincides with both the associated left and right uniformities (see IsUniformGroup.isRightUniformGroup, IsUniformGroup.isLeftUniformGroup and IsUniformGroup.of_left_right).

Since there are topological groups where these two uniformities do not coincide, not all topological groups admit a uniform group structure in this sense. This is however the case for commutative groups, which are the main motivation for the existence of this typeclass.

• uniformContinuous_div : UniformContinuous fun (p : α × α) => p.1 / p.2

class IsUniformAddGroup (α : Type u_3) [UniformSpace α] [AddGroup α] : Prop

A uniform additive group is an additive group in which addition and negation are uniformly continuous.

IsUniformAddGroup G is equivalent to the fact that G is a topological additive group, and the uniformity coincides with both the associated left and right uniformities (see IsUniformAddGroup.isRightUniformAddGroup, IsUniformAddGroup.isLeftUniformAddGroup and IsUniformAddGroup.of_left_right).

Since there are topological groups where these two uniformities do not coincide, not all topological groups admit a uniform group structure in this sense. This is however the case for commutative groups, which are the main motivation for the existence of this typeclass.

• uniformContinuous_sub : UniformContinuous fun (p : α × α) => p.1 - p.2

theorem IsUniformGroup.mk' {α : Type u_3} [UniformSpace α] [Group α] (h₁ : UniformContinuous fun (p : α × α) => p.1 * p.2) (h₂ : UniformContinuous fun (p : α) => p⁻¹) : IsUniformGroup α

theorem IsUniformAddGroup.mk' {α : Type u_3} [UniformSpace α] [AddGroup α] (h₁ : UniformContinuous fun (p : α × α) => p.1 + p.2) (h₂ : UniformContinuous fun (p : α) => -p) : IsUniformAddGroup α

theorem uniformContinuous_div {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] : UniformContinuous fun (p : α × α) => p.1 / p.2

theorem uniformContinuous_sub {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] : UniformContinuous fun (p : α × α) => p.1 - p.2

theorem UniformContinuous.div {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] [UniformSpace β] {f g : β → α} (hf : UniformContinuous f) (hg : UniformContinuous g) : UniformContinuous fun (x : β) => f x / g x

theorem UniformContinuous.sub {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] [UniformSpace β] {f g : β → α} (hf : UniformContinuous f) (hg : UniformContinuous g) : UniformContinuous fun (x : β) => f x - g x

theorem UniformContinuous.inv {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] [UniformSpace β] {f : β → α} (hf : UniformContinuous f) : UniformContinuous fun (x : β) => (f x)⁻¹

theorem UniformContinuous.neg {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] [UniformSpace β] {f : β → α} (hf : UniformContinuous f) : UniformContinuous fun (x : β) => -f x

theorem uniformContinuous_inv {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] : UniformContinuous fun (x : α) => x⁻¹

theorem uniformContinuous_neg {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] : UniformContinuous fun (x : α) => -x

theorem UniformContinuous.mul {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] [UniformSpace β] {f g : β → α} (hf : UniformContinuous f) (hg : UniformContinuous g) : UniformContinuous fun (x : β) => f x * g x

theorem UniformContinuous.add {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] [UniformSpace β] {f g : β → α} (hf : UniformContinuous f) (hg : UniformContinuous g) : UniformContinuous fun (x : β) => f x + g x

theorem uniformContinuous_mul {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] : UniformContinuous fun (p : α × α) => p.1 * p.2

theorem uniformContinuous_add {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] : UniformContinuous fun (p : α × α) => p.1 + p.2

theorem UniformContinuous.mul_const {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] [UniformSpace β] {f : β → α} (hf : UniformContinuous f) (a : α) : UniformContinuous fun (x : β) => f x * a

theorem UniformContinuous.add_const {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] [UniformSpace β] {f : β → α} (hf : UniformContinuous f) (a : α) : UniformContinuous fun (x : β) => f x + a

theorem UniformContinuous.const_mul {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] [UniformSpace β] {f : β → α} (hf : UniformContinuous f) (a : α) : UniformContinuous fun (x : β) => a * f x

theorem UniformContinuous.const_add {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] [UniformSpace β] {f : β → α} (hf : UniformContinuous f) (a : α) : UniformContinuous fun (x : β) => a + f x

theorem uniformContinuous_mul_left {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] (a : α) : UniformContinuous fun (b : α) => a * b

theorem uniformContinuous_add_left {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] (a : α) : UniformContinuous fun (b : α) => a + b

theorem uniformContinuous_mul_right {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] (a : α) : UniformContinuous fun (b : α) => b * a

theorem uniformContinuous_add_right {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] (a : α) : UniformContinuous fun (b : α) => b + a

theorem UniformContinuous.div_const {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] [UniformSpace β] {f : β → α} (hf : UniformContinuous f) (a : α) : UniformContinuous fun (x : β) => f x / a

theorem UniformContinuous.sub_const {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] [UniformSpace β] {f : β → α} (hf : UniformContinuous f) (a : α) : UniformContinuous fun (x : β) => f x - a

theorem uniformContinuous_div_const {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] (a : α) : UniformContinuous fun (b : α) => b / a

theorem uniformContinuous_sub_const {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] (a : α) : UniformContinuous fun (b : α) => b - a

theorem Filter.Tendsto.uniformity_mul {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {f g : ι → α × α} {l : Filter ι} (hf : Tendsto f l (uniformity α)) (hg : Tendsto g l (uniformity α)) : Tendsto (f * g) l (uniformity α)

theorem Filter.Tendsto.uniformity_add {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {f g : ι → α × α} {l : Filter ι} (hf : Tendsto f l (uniformity α)) (hg : Tendsto g l (uniformity α)) : Tendsto (f + g) l (uniformity α)

theorem Filter.Tendsto.uniformity_inv {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {f : ι → α × α} {l : Filter ι} (hf : Tendsto f l (uniformity α)) : Tendsto f⁻¹ l (uniformity α)

theorem Filter.Tendsto.uniformity_neg {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {f : ι → α × α} {l : Filter ι} (hf : Tendsto f l (uniformity α)) : Tendsto (-f) l (uniformity α)

theorem Filter.Tendsto.uniformity_inv_iff {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {f : ι → α × α} {l : Filter ι} : Tendsto f⁻¹ l (uniformity α) ↔ Tendsto f l (uniformity α)

theorem Filter.Tendsto.uniformity_neg_iff {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {f : ι → α × α} {l : Filter ι} : Tendsto (-f) l (uniformity α) ↔ Tendsto f l (uniformity α)

theorem Filter.Tendsto.uniformity_div {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {f g : ι → α × α} {l : Filter ι} (hf : Tendsto f l (uniformity α)) (hg : Tendsto g l (uniformity α)) : Tendsto (f / g) l (uniformity α)

theorem Filter.Tendsto.uniformity_sub {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {f g : ι → α × α} {l : Filter ι} (hf : Tendsto f l (uniformity α)) (hg : Tendsto g l (uniformity α)) : Tendsto (f - g) l (uniformity α)

theorem Filter.Tendsto.uniformity_mul_iff_right {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {f g : ι → α × α} {l : Filter ι} (hf : Tendsto f l (uniformity α)) : Tendsto (f * g) l (uniformity α) ↔ Tendsto g l (uniformity α)

If f : ι → G × G converges to the uniformity, then any g : ι → G × G converges to the uniformity iff f * g does. This is often useful when f is valued in the diagonal, in which case its convergence is automatic.

theorem Filter.Tendsto.uniformity_add_iff_right {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {f g : ι → α × α} {l : Filter ι} (hf : Tendsto f l (uniformity α)) : Tendsto (f + g) l (uniformity α) ↔ Tendsto g l (uniformity α)

If f : ι → G × G converges to the uniformity, then any g : ι → G × G converges to the uniformity iff f + g does. This is often useful when f is valued in the diagonal, in which case its convergence is automatic.

theorem Filter.Tendsto.uniformity_mul_iff_left {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {f g : ι → α × α} {l : Filter ι} (hg : Tendsto g l (uniformity α)) : Tendsto (f * g) l (uniformity α) ↔ Tendsto f l (uniformity α)

If g : ι → G × G converges to the uniformity, then any f : ι → G × G converges to the uniformity iff f * g does. This is often useful when g is valued in the diagonal, in which case its convergence is automatic.

theorem Filter.Tendsto.uniformity_add_iff_left {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {f g : ι → α × α} {l : Filter ι} (hg : Tendsto g l (uniformity α)) : Tendsto (f + g) l (uniformity α) ↔ Tendsto f l (uniformity α)

If g : ι → G × G converges to the uniformity, then any f : ι → G × G converges to the uniformity iff f + g does. This is often useful when g is valued in the diagonal, in which case its convergence is automatic.

theorem UniformContinuous.pow_const {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] [UniformSpace β] {f : β → α} (hf : UniformContinuous f) (n : ℕ) : UniformContinuous fun (x : β) => f x ^ n

theorem UniformContinuous.const_nsmul {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] [UniformSpace β] {f : β → α} (hf : UniformContinuous f) (n : ℕ) : UniformContinuous fun (x : β) => n • f x

theorem uniformContinuous_pow_const {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] (n : ℕ) : UniformContinuous fun (x : α) => x ^ n

theorem uniformContinuous_const_nsmul {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] (n : ℕ) : UniformContinuous fun (x : α) => n • x

theorem UniformContinuous.zpow_const {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] [UniformSpace β] {f : β → α} (hf : UniformContinuous f) (n : ℤ) : UniformContinuous fun (x : β) => f x ^ n

theorem UniformContinuous.const_zsmul {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] [UniformSpace β] {f : β → α} (hf : UniformContinuous f) (n : ℤ) : UniformContinuous fun (x : β) => n • f x

theorem uniformContinuous_zpow_const {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] (n : ℤ) : UniformContinuous fun (x : α) => x ^ n

theorem uniformContinuous_const_zsmul {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] (n : ℤ) : UniformContinuous fun (x : α) => n • x

@[instance 10]

instance IsUniformGroup.to_topologicalGroup {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] : IsTopologicalGroup α

@[instance 10]

instance IsUniformAddGroup.to_topologicalAddGroup {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] : IsTopologicalAddGroup α

theorem uniformity_translate_mul {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] (a : α) : Filter.map (fun (x : α × α) => (x.1 * a, x.2 * a)) (uniformity α) = uniformity α

theorem uniformity_translate_add {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] (a : α) : Filter.map (fun (x : α × α) => (x.1 + a, x.2 + a)) (uniformity α) = uniformity α

instance MulOpposite.instIsUniformGroup {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] : IsUniformGroup αᵐᵒᵖ

instance AddOpposite.instIsUniformAddGroup {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] : IsUniformAddGroup αᵃᵒᵖ

instance IsUniformGroup.isRightUniformGroup (α : Type u_1) [UniformSpace α] [Group α] [IsUniformGroup α] : IsRightUniformGroup α

instance IsUniformAddGroup.isRightUniformAddGroup (α : Type u_1) [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] : IsRightUniformAddGroup α

instance IsUniformGroup.isLeftUniformGroup (α : Type u_1) [UniformSpace α] [Group α] [IsUniformGroup α] : IsLeftUniformGroup α

instance IsUniformAddGroup.isLeftUniformAddGroup (α : Type u_1) [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] : IsLeftUniformAddGroup α

theorem IsUniformGroup.ext {G : Type u_3} [Group G] {u v : UniformSpace G} (hu : IsUniformGroup G) (hv : IsUniformGroup G) (h : nhds 1 = nhds 1) : u = v

theorem IsUniformAddGroup.ext {G : Type u_3} [AddGroup G] {u v : UniformSpace G} (hu : IsUniformAddGroup G) (hv : IsUniformAddGroup G) (h : nhds 0 = nhds 0) : u = v

theorem IsUniformGroup.ext_iff {G : Type u_3} [Group G] {u v : UniformSpace G} (hu : IsUniformGroup G) (hv : IsUniformGroup G) : u = v ↔ nhds 1 = nhds 1

theorem IsUniformAddGroup.ext_iff {G : Type u_3} [AddGroup G] {u v : UniformSpace G} (hu : IsUniformAddGroup G) (hv : IsUniformAddGroup G) : u = v ↔ nhds 0 = nhds 0

theorem IsUniformGroup.uniformity_countably_generated {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] [(nhds 1).IsCountablyGenerated] : (uniformity α).IsCountablyGenerated

theorem IsUniformAddGroup.uniformity_countably_generated {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] [(nhds 0).IsCountablyGenerated] : (uniformity α).IsCountablyGenerated

theorem comap_conj_nhds_one {β : Type u_2} [UniformSpace β] [Group β] [IsLeftUniformGroup β] [IsRightUniformGroup β] : Filter.comap (fun (gx : β × β) => gx.1 * gx.2 * gx.1⁻¹) (nhds 1) = Filter.comap Prod.snd (nhds 1)

Note: this assumes [IsLeftUniformGroup β] [IsRightUniformGroup β] instead of the more typical (and equivalent) [IsUniformGroup β] because this is used in the proof of said equivalence.

theorem comap_conj_nhds_zero {β : Type u_2} [UniformSpace β] [AddGroup β] [IsLeftUniformAddGroup β] [IsRightUniformAddGroup β] : Filter.comap (fun (gx : β × β) => gx.1 + gx.2 + -gx.1) (nhds 0) = Filter.comap Prod.snd (nhds 0)

Note: this assumes [IsLeftUniformAddGroup β] [IsRightUniformAddGroup β] instead of the more typical (and equivalent) [IsUniformAddGroup β] because this is used in the proof of said equivalence.

theorem tendsto_conj_nhds_one {β : Type u_2} [UniformSpace β] [Group β] [IsLeftUniformGroup β] [IsRightUniformGroup β] : Filter.Tendsto (fun (gx : β × β) => gx.1 * gx.2 * gx.1⁻¹) (Filter.comap Prod.snd (nhds 1)) (nhds 1)

Note: this assumes [IsLeftUniformGroup β] [IsRightUniformGroup β] instead of the more typical (and equivalent) [IsUniformGroup β] because this is used in the proof of said equivalence.

theorem tendsto_conj_nhds_zero {β : Type u_2} [UniformSpace β] [AddGroup β] [IsLeftUniformAddGroup β] [IsRightUniformAddGroup β] : Filter.Tendsto (fun (gx : β × β) => gx.1 + gx.2 + -gx.1) (Filter.comap Prod.snd (nhds 0)) (nhds 0)

Note: this assumes [IsLeftUniformAddGroup β] [IsRightUniformAddGroup β] instead of the more typical (and equivalent) [IsUniformAddGroup β] because this is used in the proof of said equivalence.

theorem Filter.Tendsto.conj_nhds_one {β : Type u_2} [UniformSpace β] [Group β] [IsLeftUniformGroup β] [IsRightUniformGroup β] {ι : Type u_3} {l : Filter ι} {x : ι → β} (hx : Tendsto x l (nhds 1)) (g : ι → β) : Tendsto (g * x * g⁻¹) l (nhds 1)

Note: this assumes [IsLeftUniformGroup β] [IsRightUniformGroup β] instead of the more typical (and equivalent) [IsUniformGroup β] because this is used in the proof of said equivalence.

theorem Filter.Tendsto.conj_nhds_zero {β : Type u_2} [UniformSpace β] [AddGroup β] [IsLeftUniformAddGroup β] [IsRightUniformAddGroup β] {ι : Type u_3} {l : Filter ι} {x : ι → β} (hx : Tendsto x l (nhds 0)) (g : ι → β) : Tendsto (g + x + -g) l (nhds 0)

Note: this assumes [IsLeftUniformAddGroup β] [IsRightUniformAddGroup β] instead of the more typical (and equivalent) [IsUniformAddGroup β] because this is used in the proof of said equivalence.

theorem IsUniformGroup.of_left_right {β : Type u_2} [UniformSpace β] [Group β] [IsLeftUniformGroup β] [IsRightUniformGroup β] : IsUniformGroup β

theorem isUniformGroup_iff_left_right {γ : Type u_3} [Group γ] [UniformSpace γ] : IsUniformGroup γ ↔ IsLeftUniformGroup γ ∧ IsRightUniformGroup γ

theorem eventually_forall_conj_nhds_one {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] {p : α → Prop} (hp : ∀ᶠ (x : α) in nhds 1, p x) : ∀ᶠ (x : α) in nhds 1, ∀ (g : α), p (g * x * g⁻¹)

theorem Filter.HasBasis.uniformity_of_nhds_one {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Sort u_3} {p : ι → Prop} {U : ι → Set α} (h : (nhds 1).HasBasis p U) : (uniformity α).HasBasis p fun (i : ι) => {x : α × α | x.2 / x.1 ∈ U i}

theorem Filter.HasBasis.uniformity_of_nhds_zero {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Sort u_3} {p : ι → Prop} {U : ι → Set α} (h : (nhds 0).HasBasis p U) : (uniformity α).HasBasis p fun (i : ι) => {x : α × α | x.2 - x.1 ∈ U i}

theorem Filter.HasBasis.uniformity_of_nhds_one_inv_mul {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Sort u_3} {p : ι → Prop} {U : ι → Set α} (h : (nhds 1).HasBasis p U) : (uniformity α).HasBasis p fun (i : ι) => {x : α × α | x.1⁻¹ * x.2 ∈ U i}

theorem Filter.HasBasis.uniformity_of_nhds_zero_neg_add {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Sort u_3} {p : ι → Prop} {U : ι → Set α} (h : (nhds 0).HasBasis p U) : (uniformity α).HasBasis p fun (i : ι) => {x : α × α | -x.1 + x.2 ∈ U i}

theorem Filter.HasBasis.uniformity_of_nhds_one_swapped {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Sort u_3} {p : ι → Prop} {U : ι → Set α} (h : (nhds 1).HasBasis p U) : (uniformity α).HasBasis p fun (i : ι) => {x : α × α | x.1 / x.2 ∈ U i}

theorem Filter.HasBasis.uniformity_of_nhds_zero_swapped {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Sort u_3} {p : ι → Prop} {U : ι → Set α} (h : (nhds 0).HasBasis p U) : (uniformity α).HasBasis p fun (i : ι) => {x : α × α | x.1 - x.2 ∈ U i}

theorem Filter.HasBasis.uniformity_of_nhds_one_inv_mul_swapped {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Sort u_3} {p : ι → Prop} {U : ι → Set α} (h : (nhds 1).HasBasis p U) : (uniformity α).HasBasis p fun (i : ι) => {x : α × α | x.2⁻¹ * x.1 ∈ U i}

theorem Filter.HasBasis.uniformity_of_nhds_zero_neg_add_swapped {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Sort u_3} {p : ι → Prop} {U : ι → Set α} (h : (nhds 0).HasBasis p U) : (uniformity α).HasBasis p fun (i : ι) => {x : α × α | -x.2 + x.1 ∈ U i}

theorem uniformContinuous_of_tendsto_one {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] {hom : Type u_3} [UniformSpace β] [Group β] [IsUniformGroup β] [FunLike hom α β] [MonoidHomClass hom α β] {f : hom} (h : Filter.Tendsto (⇑f) (nhds 1) (nhds 1)) : UniformContinuous ⇑f

theorem uniformContinuous_of_tendsto_zero {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {hom : Type u_3} [UniformSpace β] [AddGroup β] [IsUniformAddGroup β] [FunLike hom α β] [AddMonoidHomClass hom α β] {f : hom} (h : Filter.Tendsto (⇑f) (nhds 0) (nhds 0)) : UniformContinuous ⇑f

theorem uniformContinuous_of_continuousAt_one {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] {hom : Type u_3} [UniformSpace β] [Group β] [IsUniformGroup β] [FunLike hom α β] [MonoidHomClass hom α β] (f : hom) (hf : ContinuousAt (⇑f) 1) : UniformContinuous ⇑f

A group homomorphism (a bundled morphism of a type that implements MonoidHomClass) between two uniform groups is uniformly continuous provided that it is continuous at one. See also continuous_of_continuousAt_one.

theorem uniformContinuous_of_continuousAt_zero {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {hom : Type u_3} [UniformSpace β] [AddGroup β] [IsUniformAddGroup β] [FunLike hom α β] [AddMonoidHomClass hom α β] (f : hom) (hf : ContinuousAt (⇑f) 0) : UniformContinuous ⇑f

An additive group homomorphism (a bundled morphism of a type that implements AddMonoidHomClass) between two uniform additive groups is uniformly continuous provided that it is continuous at zero. See also continuous_of_continuousAt_zero.

theorem MonoidHom.uniformContinuous_of_continuousAt_one {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] [UniformSpace β] [Group β] [IsUniformGroup β] (f : α →* β) (hf : ContinuousAt (⇑f) 1) : UniformContinuous ⇑f

theorem AddMonoidHom.uniformContinuous_of_continuousAt_zero {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] [UniformSpace β] [AddGroup β] [IsUniformAddGroup β] (f : α →+ β) (hf : ContinuousAt (⇑f) 0) : UniformContinuous ⇑f

theorem IsUniformGroup.uniformContinuous_iff_isOpen_ker {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] {hom : Type u_3} [UniformSpace β] [DiscreteTopology β] [Group β] [IsUniformGroup β] [FunLike hom α β] [MonoidHomClass hom α β] {f : hom} : UniformContinuous ⇑f ↔ IsOpen ↑(↑f).ker

A homomorphism from a uniform group to a discrete uniform group is continuous if and only if its kernel is open.

theorem IsUniformAddGroup.uniformContinuous_iff_isOpen_ker {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {hom : Type u_3} [UniformSpace β] [DiscreteTopology β] [AddGroup β] [IsUniformAddGroup β] [FunLike hom α β] [AddMonoidHomClass hom α β] {f : hom} : UniformContinuous ⇑f ↔ IsOpen ↑(↑f).ker

A homomorphism from a uniform additive group to a discrete uniform additive group is continuous if and only if its kernel is open.

theorem uniformContinuous_monoidHom_of_continuous {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] {hom : Type u_3} [UniformSpace β] [Group β] [IsUniformGroup β] [FunLike hom α β] [MonoidHomClass hom α β] {f : hom} (h : Continuous ⇑f) : UniformContinuous ⇑f

theorem uniformContinuous_addMonoidHom_of_continuous {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {hom : Type u_3} [UniformSpace β] [AddGroup β] [IsUniformAddGroup β] [FunLike hom α β] [AddMonoidHomClass hom α β] {f : hom} (h : Continuous ⇑f) : UniformContinuous ⇑f

def IsTopologicalGroup.rightUniformSpace (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : UniformSpace G

The right uniformity on a topological group (as opposed to the left uniformity).

Warning: in general the right and left uniformities do not coincide and so one does not obtain a IsUniformGroup structure. Two important special cases where they do coincide are for commutative groups (see isUniformGroup_of_commGroup) and for compact groups (see IsUniformGroup.of_compactSpace).

Equations

• One or more equations did not get rendered due to their size.

def IsTopologicalAddGroup.rightUniformSpace (G : Type u_1) [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] : UniformSpace G

The right uniformity on a topological additive group (as opposed to the left uniformity).

Warning: in general the right and left uniformities do not coincide and so one does not obtain a IsUniformAddGroup structure. Two important special cases where they do coincide are for commutative additive groups (see isUniformAddGroup_of_addCommGroup) and for compact additive groups (see IsUniformAddGroup.of_compactSpace).

Equations

• One or more equations did not get rendered due to their size.

@[deprecated IsTopologicalAddGroup.rightUniformSpace (since := "2025-09-26")]

def IsTopologicalAddGroup.toUniformSpace (G : Type u_1) [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] : UniformSpace G

Alias of IsTopologicalAddGroup.rightUniformSpace.

---

The right uniformity on a topological additive group (as opposed to the left uniformity).

Warning: in general the right and left uniformities do not coincide and so one does not obtain a IsUniformAddGroup structure. Two important special cases where they do coincide are for commutative additive groups (see isUniformAddGroup_of_addCommGroup) and for compact additive groups (see IsUniformAddGroup.of_compactSpace).

Equations

• IsTopologicalAddGroup.toUniformSpace = IsTopologicalAddGroup.rightUniformSpace

@[deprecated IsTopologicalGroup.rightUniformSpace (since := "2025-09-26")]

def IsTopologicalGroup.toUniformSpace (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : UniformSpace G

Alias of IsTopologicalGroup.rightUniformSpace.

---

The right uniformity on a topological group (as opposed to the left uniformity).

Warning: in general the right and left uniformities do not coincide and so one does not obtain a IsUniformGroup structure. Two important special cases where they do coincide are for commutative groups (see isUniformGroup_of_commGroup) and for compact groups (see IsUniformGroup.of_compactSpace).

Equations

• IsTopologicalGroup.toUniformSpace = IsTopologicalGroup.rightUniformSpace

theorem uniformity_eq_comap_nhds_one' (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : uniformity G = Filter.comap (fun (p : G × G) => p.2 / p.1) (nhds 1)

theorem uniformity_eq_comap_nhds_zero' (G : Type u_1) [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] : uniformity G = Filter.comap (fun (p : G × G) => p.2 - p.1) (nhds 0)

theorem isUniformGroup_of_commGroup {G : Type u_1} [CommGroup G] [TopologicalSpace G] [IsTopologicalGroup G] : IsUniformGroup G

theorem isUniformAddGroup_of_addCommGroup {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] : IsUniformAddGroup G

theorem comm_topologicalGroup_is_uniform {G : Type u_1} [CommGroup G] [TopologicalSpace G] [IsTopologicalGroup G] : IsUniformGroup G

Alias of isUniformGroup_of_commGroup.

theorem IsUniformGroup.rightUniformSpace_eq {G : Type u_2} [u : UniformSpace G] [Group G] [IsUniformGroup G] : IsTopologicalGroup.rightUniformSpace G = u

theorem IsUniformAddGroup.rightUniformSpace_eq {G : Type u_2} [u : UniformSpace G] [AddGroup G] [IsUniformAddGroup G] : IsTopologicalAddGroup.rightUniformSpace G = u

@[deprecated IsUniformAddGroup.rightUniformSpace_eq (since := "2025-09-26")]

theorem IsUniformAddGroup.toUniformSpace_eq {G : Type u_2} [u : UniformSpace G] [AddGroup G] [IsUniformAddGroup G] : IsTopologicalAddGroup.rightUniformSpace G = u

Alias of IsUniformAddGroup.rightUniformSpace_eq.

@[deprecated IsUniformGroup.rightUniformSpace_eq (since := "2025-09-26")]

theorem IsUniformGroup.toUniformSpace_eq {G : Type u_2} [u : UniformSpace G] [Group G] [IsUniformGroup G] : IsTopologicalGroup.rightUniformSpace G = u

Alias of IsUniformGroup.rightUniformSpace_eq.