Uniform structure on topological groups

This file defines uniform groups and its additive counterpart. These typeclasses should be preferred over using [TopologicalSpace α] [IsTopologicalGroup α] since every topological group naturally induces a uniform structure.

Main declarations

• IsUniformGroup and IsUniformAddGroup: Multiplicative and additive uniform groups, i.e., groups with uniformly continuous (*) and (⁻¹) / (+) and (-).

Main results

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

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

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

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

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

@[deprecated IsUniformGroup (since := "2025-03-26")]

def UniformGroup (α : Type u_3) [UniformSpace α] [Group α] : Prop

Alias of IsUniformGroup.

---

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

Equations

• UniformGroup = IsUniformGroup

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

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

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

@[deprecated IsUniformAddGroup (since := "2025-03-26")]

def UniformAddGroup (α : Type u_3) [UniformSpace α] [AddGroup α] : Prop

Alias of IsUniformAddGroup.

---

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

Equations

• UniformAddGroup = IsUniformAddGroup

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 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 α

@[deprecated IsUniformAddGroup.to_topologicalAddGroup (since := "2025-03-31")]

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

Alias of IsUniformAddGroup.to_topologicalAddGroup.

@[deprecated IsUniformGroup.to_topologicalGroup (since := "2025-03-31")]

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

Alias of IsUniformGroup.to_topologicalGroup.

instance Prod.instIsUniformGroup {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] [UniformSpace β] [Group β] [IsUniformGroup β] : IsUniformGroup (α × β)

instance Prod.instIsUniformAddGroup {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] [UniformSpace β] [AddGroup β] [IsUniformAddGroup β] : IsUniformAddGroup (α × β)

@[deprecated Prod.instIsUniformAddGroup (since := "2025-03-31")]

theorem Prod.instUniformAddGroup {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] [UniformSpace β] [AddGroup β] [IsUniformAddGroup β] : IsUniformAddGroup (α × β)

Alias of Prod.instIsUniformAddGroup.

@[deprecated Prod.instIsUniformGroup (since := "2025-03-31")]

theorem Prod.instUniformGroup {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] [UniformSpace β] [Group β] [IsUniformGroup β] : IsUniformGroup (α × β)

Alias of Prod.instIsUniformGroup.

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 αᵃᵒᵖ

theorem isUniformGroup_sInf {β : Type u_2} [Group β] {us : Set (UniformSpace β)} (h : ∀ u ∈ us, IsUniformGroup β) : IsUniformGroup β

theorem isUniformAddGroup_sInf {β : Type u_2} [AddGroup β] {us : Set (UniformSpace β)} (h : ∀ u ∈ us, IsUniformAddGroup β) : IsUniformAddGroup β

@[deprecated isUniformAddGroup_sInf (since := "2025-03-31")]

theorem uniformAddGroup_sInf {β : Type u_2} [AddGroup β] {us : Set (UniformSpace β)} (h : ∀ u ∈ us, IsUniformAddGroup β) : IsUniformAddGroup β

Alias of isUniformAddGroup_sInf.

@[deprecated isUniformGroup_sInf (since := "2025-03-31")]

theorem uniformGroup_sInf {β : Type u_2} [Group β] {us : Set (UniformSpace β)} (h : ∀ u ∈ us, IsUniformGroup β) : IsUniformGroup β

Alias of isUniformGroup_sInf.

theorem isUniformGroup_iInf {β : Type u_2} [Group β] {ι : Sort u_3} {us' : ι → UniformSpace β} (h' : ∀ (i : ι), IsUniformGroup β) : IsUniformGroup β

theorem isUniformAddGroup_iInf {β : Type u_2} [AddGroup β] {ι : Sort u_3} {us' : ι → UniformSpace β} (h' : ∀ (i : ι), IsUniformAddGroup β) : IsUniformAddGroup β

@[deprecated isUniformAddGroup_iInf (since := "2025-03-31")]

theorem uniformAddGroup_iInf {β : Type u_2} [AddGroup β] {ι : Sort u_3} {us' : ι → UniformSpace β} (h' : ∀ (i : ι), IsUniformAddGroup β) : IsUniformAddGroup β

Alias of isUniformAddGroup_iInf.

@[deprecated isUniformGroup_iInf (since := "2025-03-31")]

theorem uniformGroup_iInf {β : Type u_2} [Group β] {ι : Sort u_3} {us' : ι → UniformSpace β} (h' : ∀ (i : ι), IsUniformGroup β) : IsUniformGroup β

Alias of isUniformGroup_iInf.

theorem isUniformGroup_inf {β : Type u_2} [Group β] {u₁ u₂ : UniformSpace β} (h₁ : IsUniformGroup β) (h₂ : IsUniformGroup β) : IsUniformGroup β

theorem isUniformAddGroup_inf {β : Type u_2} [AddGroup β] {u₁ u₂ : UniformSpace β} (h₁ : IsUniformAddGroup β) (h₂ : IsUniformAddGroup β) : IsUniformAddGroup β

@[deprecated isUniformAddGroup_inf (since := "2025-03-31")]

theorem uniformAddGroup_inf {β : Type u_2} [AddGroup β] {u₁ u₂ : UniformSpace β} (h₁ : IsUniformAddGroup β) (h₂ : IsUniformAddGroup β) : IsUniformAddGroup β

Alias of isUniformAddGroup_inf.

@[deprecated isUniformGroup_inf (since := "2025-03-31")]

theorem uniformGroup_inf {β : Type u_2} [Group β] {u₁ u₂ : UniformSpace β} (h₁ : IsUniformGroup β) (h₂ : IsUniformGroup β) : IsUniformGroup β

Alias of isUniformGroup_inf.

theorem uniformity_eq_comap_nhds_one (α : Type u_1) [UniformSpace α] [Group α] [IsUniformGroup α] : uniformity α = Filter.comap (fun (x : α × α) => x.2 / x.1) (nhds 1)

theorem uniformity_eq_comap_nhds_zero (α : Type u_1) [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] : uniformity α = Filter.comap (fun (x : α × α) => x.2 - x.1) (nhds 0)

theorem uniformity_eq_comap_nhds_one_swapped (α : Type u_1) [UniformSpace α] [Group α] [IsUniformGroup α] : uniformity α = Filter.comap (fun (x : α × α) => x.1 / x.2) (nhds 1)

theorem uniformity_eq_comap_nhds_zero_swapped (α : Type u_1) [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] : uniformity α = Filter.comap (fun (x : α × α) => x.1 - x.2) (nhds 0)

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

@[deprecated IsUniformAddGroup.ext (since := "2025-03-31")]

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

Alias of IsUniformAddGroup.ext.

@[deprecated IsUniformGroup.ext (since := "2025-03-31")]

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

Alias of IsUniformGroup.ext.

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

@[deprecated IsUniformAddGroup.ext_iff (since := "2025-03-31")]

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

Alias of IsUniformAddGroup.ext_iff.

@[deprecated IsUniformGroup.ext_iff (since := "2025-03-31")]

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

Alias of IsUniformGroup.ext_iff.

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

@[deprecated IsUniformAddGroup.uniformity_countably_generated (since := "2025-03-31")]

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

Alias of IsUniformAddGroup.uniformity_countably_generated.

@[deprecated IsUniformGroup.uniformity_countably_generated (since := "2025-03-31")]

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

Alias of IsUniformGroup.uniformity_countably_generated.

theorem uniformity_eq_comap_inv_mul_nhds_one {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] : uniformity α = Filter.comap (fun (x : α × α) => x.1⁻¹ * x.2) (nhds 1)

theorem uniformity_eq_comap_neg_add_nhds_zero {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] : uniformity α = Filter.comap (fun (x : α × α) => -x.1 + x.2) (nhds 0)

theorem uniformity_eq_comap_inv_mul_nhds_one_swapped {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] : uniformity α = Filter.comap (fun (x : α × α) => x.2⁻¹ * x.1) (nhds 1)

theorem uniformity_eq_comap_neg_add_nhds_zero_swapped {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] : uniformity α = Filter.comap (fun (x : α × α) => -x.2 + x.1) (nhds 0)

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.

@[deprecated IsUniformAddGroup.uniformContinuous_iff_isOpen_ker (since := "2024-11-18")]

theorem UniformAddGroup.uniformContinuous_iff_open_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

Alias of IsUniformAddGroup.uniformContinuous_iff_isOpen_ker.

---

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

@[deprecated IsUniformGroup.uniformContinuous_iff_isOpen_ker (since := "2024-11-18")]

theorem UniformGroup.uniformContinuous_iff_open_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

Alias of IsUniformGroup.uniformContinuous_iff_isOpen_ker.

---

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

@[deprecated IsUniformAddGroup.uniformContinuous_iff_isOpen_ker (since := "2025-03-30")]

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

Alias of IsUniformAddGroup.uniformContinuous_iff_isOpen_ker.

---

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

@[deprecated IsUniformGroup.uniformContinuous_iff_isOpen_ker (since := "2025-03-30")]

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

Alias of IsUniformGroup.uniformContinuous_iff_isOpen_ker.

---

A homomorphism from a uniform group to a discrete uniform 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.toUniformSpace (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 comm_topologicalGroup_is_uniform) and for compact groups (see topologicalGroup_is_uniform_of_compactSpace).

Equations

• IsTopologicalGroup.toUniformSpace G = UniformSpace.mk (Filter.comap (fun (p : G × G) => p.2 / p.1) (nhds 1)) ⋯ ⋯ ⋯

def IsTopologicalAddGroup.toUniformSpace (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 comm_topologicalAddGroup_is_uniform) and for compact additive groups (see topologicalAddGroup_is_uniform_of_compactSpace).

Equations

• IsTopologicalAddGroup.toUniformSpace G = UniformSpace.mk (Filter.comap (fun (p : G × G) => p.2 - p.1) (nhds 0)) ⋯ ⋯ ⋯

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

@[deprecated isUniformAddGroup_of_addCommGroup (since := "2025-02-28")]

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

Alias of isUniformAddGroup_of_addCommGroup.

@[deprecated isUniformGroup_of_commGroup (since := "2025-02-28")]

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

Alias of isUniformGroup_of_commGroup.

@[deprecated isUniformAddGroup_of_addCommGroup (since := "2025-03-30")]

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

Alias of isUniformAddGroup_of_addCommGroup.

@[deprecated isUniformGroup_of_commGroup (since := "2025-03-30")]

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

Alias of isUniformGroup_of_commGroup.

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

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

theorem tendsto_div_comap_self {α : Type u_1} {β : Type u_2} {hom : Type u_3} [TopologicalSpace α] [Group α] [IsTopologicalGroup α] [TopologicalSpace β] [Group β] [FunLike hom β α] [MonoidHomClass hom β α] {e : hom} (de : IsDenseInducing ⇑e) (x₀ : α) : Filter.Tendsto (fun (t : β × β) => t.2 / t.1) (Filter.comap (fun (p : β × β) => (e p.1, e p.2)) (nhds (x₀, x₀))) (nhds 1)

theorem tendsto_sub_comap_self {α : Type u_1} {β : Type u_2} {hom : Type u_3} [TopologicalSpace α] [AddGroup α] [IsTopologicalAddGroup α] [TopologicalSpace β] [AddGroup β] [FunLike hom β α] [AddMonoidHomClass hom β α] {e : hom} (de : IsDenseInducing ⇑e) (x₀ : α) : Filter.Tendsto (fun (t : β × β) => t.2 - t.1) (Filter.comap (fun (p : β × β) => (e p.1, e p.2)) (nhds (x₀, x₀))) (nhds 0)