Documentation

Mathlib.Topology.Algebra.UniformGroup

Uniform structure on topological groups #

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

Main declarations #

Main results #

class UniformGroup (α : Type u_3) [UniformSpace α] [Group α] :

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

Instances
    theorem UniformGroup.uniformContinuous_div {α : Type u_3} :
    ∀ {inst : UniformSpace α} {inst_1 : Group α} [self : UniformGroup α], UniformContinuous fun (p : α × α) => p.1 / p.2
    class UniformAddGroup (α : Type u_3) [UniformSpace α] [AddGroup α] :

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

    Instances
      theorem UniformAddGroup.uniformContinuous_sub {α : Type u_3} :
      ∀ {inst : UniformSpace α} {inst_1 : AddGroup α} [self : UniformAddGroup α], UniformContinuous fun (p : α × α) => p.1 - p.2
      theorem UniformAddGroup.mk' {α : Type u_3} [UniformSpace α] [AddGroup α] (h₁ : UniformContinuous fun (p : α × α) => p.1 + p.2) (h₂ : UniformContinuous fun (p : α) => -p) :
      theorem UniformGroup.mk' {α : Type u_3} [UniformSpace α] [Group α] (h₁ : UniformContinuous fun (p : α × α) => p.1 * p.2) (h₂ : UniformContinuous fun (p : α) => p⁻¹) :
      theorem uniformContinuous_sub {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] :
      UniformContinuous fun (p : α × α) => p.1 - p.2
      theorem uniformContinuous_div {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] :
      UniformContinuous fun (p : α × α) => p.1 / p.2
      theorem UniformContinuous.sub {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] [UniformSpace β] {f : βα} {g : βα} (hf : UniformContinuous f) (hg : UniformContinuous g) :
      UniformContinuous fun (x : β) => f x - g x
      theorem UniformContinuous.div {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] [UniformSpace β] {f : βα} {g : βα} (hf : UniformContinuous f) (hg : UniformContinuous g) :
      UniformContinuous fun (x : β) => f x / g x
      theorem UniformContinuous.neg {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] [UniformSpace β] {f : βα} (hf : UniformContinuous f) :
      UniformContinuous fun (x : β) => -f x
      theorem UniformContinuous.inv {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] [UniformSpace β] {f : βα} (hf : UniformContinuous f) :
      UniformContinuous fun (x : β) => (f x)⁻¹
      theorem uniformContinuous_neg {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] :
      UniformContinuous fun (x : α) => -x
      theorem uniformContinuous_inv {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] :
      UniformContinuous fun (x : α) => x⁻¹
      theorem UniformContinuous.add {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] [UniformSpace β] {f : βα} {g : βα} (hf : UniformContinuous f) (hg : UniformContinuous g) :
      UniformContinuous fun (x : β) => f x + g x
      theorem UniformContinuous.mul {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] [UniformSpace β] {f : βα} {g : βα} (hf : UniformContinuous f) (hg : UniformContinuous g) :
      UniformContinuous fun (x : β) => f x * g x
      theorem uniformContinuous_add {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] :
      UniformContinuous fun (p : α × α) => p.1 + p.2
      theorem uniformContinuous_mul {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] :
      UniformContinuous fun (p : α × α) => p.1 * p.2
      theorem UniformContinuous.add_const {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] [UniformSpace β] {f : βα} (hf : UniformContinuous f) (a : α) :
      UniformContinuous fun (x : β) => f x + a
      theorem UniformContinuous.mul_const {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] [UniformSpace β] {f : βα} (hf : UniformContinuous f) (a : α) :
      UniformContinuous fun (x : β) => f x * a
      theorem UniformContinuous.const_add {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] [UniformSpace β] {f : βα} (hf : UniformContinuous f) (a : α) :
      UniformContinuous fun (x : β) => a + f x
      theorem UniformContinuous.const_mul {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] [UniformSpace β] {f : βα} (hf : UniformContinuous f) (a : α) :
      UniformContinuous fun (x : β) => a * f x
      theorem uniformContinuous_add_left {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] (a : α) :
      UniformContinuous fun (b : α) => a + b
      theorem uniformContinuous_mul_left {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] (a : α) :
      UniformContinuous fun (b : α) => a * b
      theorem uniformContinuous_add_right {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] (a : α) :
      UniformContinuous fun (b : α) => b + a
      theorem uniformContinuous_mul_right {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] (a : α) :
      UniformContinuous fun (b : α) => b * a
      theorem UniformContinuous.sub_const {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] [UniformSpace β] {f : βα} (hf : UniformContinuous f) (a : α) :
      UniformContinuous fun (x : β) => f x - a
      theorem UniformContinuous.div_const {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] [UniformSpace β] {f : βα} (hf : UniformContinuous f) (a : α) :
      UniformContinuous fun (x : β) => f x / a
      theorem uniformContinuous_sub_const {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] (a : α) :
      UniformContinuous fun (b : α) => b - a
      theorem uniformContinuous_div_const {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] (a : α) :
      UniformContinuous fun (b : α) => b / a
      theorem UniformContinuous.const_nsmul {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] [UniformSpace β] {f : βα} (hf : UniformContinuous f) (n : ) :
      UniformContinuous fun (x : β) => n f x
      theorem UniformContinuous.pow_const {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] [UniformSpace β] {f : βα} (hf : UniformContinuous f) (n : ) :
      UniformContinuous fun (x : β) => f x ^ n
      theorem uniformContinuous_const_nsmul {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] (n : ) :
      UniformContinuous fun (x : α) => n x
      theorem uniformContinuous_pow_const {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] (n : ) :
      UniformContinuous fun (x : α) => x ^ n
      theorem UniformContinuous.const_zsmul {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] [UniformSpace β] {f : βα} (hf : UniformContinuous f) (n : ) :
      UniformContinuous fun (x : β) => n f x
      theorem UniformContinuous.zpow_const {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] [UniformSpace β] {f : βα} (hf : UniformContinuous f) (n : ) :
      UniformContinuous fun (x : β) => f x ^ n
      theorem uniformContinuous_const_zsmul {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] (n : ) :
      UniformContinuous fun (x : α) => n x
      theorem uniformContinuous_zpow_const {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] (n : ) :
      UniformContinuous fun (x : α) => x ^ n
      @[instance 10]
      Equations
      • =
      @[instance 10]
      Equations
      • =
      instance instUniformAddGroupSum {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] [UniformSpace β] [AddGroup β] [UniformAddGroup β] :
      Equations
      • =
      instance instUniformGroupProd {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] [UniformSpace β] [Group β] [UniformGroup β] :
      Equations
      • =
      instance Pi.instUniformAddGroup {ι : Type u_3} {G : ιType u_4} [(i : ι) → UniformSpace (G i)] [(i : ι) → AddGroup (G i)] [∀ (i : ι), UniformAddGroup (G i)] :
      UniformAddGroup ((i : ι) → G i)
      Equations
      • =
      instance Pi.instUniformGroup {ι : Type u_3} {G : ιType u_4} [(i : ι) → UniformSpace (G i)] [(i : ι) → Group (G i)] [∀ (i : ι), UniformGroup (G i)] :
      UniformGroup ((i : ι) → G i)
      Equations
      • =
      theorem uniformity_translate_add {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] (a : α) :
      Filter.map (fun (x : α × α) => (x.1 + a, x.2 + a)) (uniformity α) = uniformity α
      theorem uniformity_translate_mul {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] (a : α) :
      Filter.map (fun (x : α × α) => (x.1 * a, x.2 * a)) (uniformity α) = uniformity α
      theorem isUniformEmbedding_translate_add {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] (a : α) :
      IsUniformEmbedding fun (x : α) => x + a
      theorem isUniformEmbedding_translate_mul {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] (a : α) :
      IsUniformEmbedding fun (x : α) => x * a
      @[deprecated isUniformEmbedding_translate_mul]
      theorem uniformEmbedding_translate_mul {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] (a : α) :
      IsUniformEmbedding fun (x : α) => x * a

      Alias of isUniformEmbedding_translate_mul.

      Equations
      • =
      theorem uniformAddGroup_sInf {β : Type u_2} [AddGroup β] {us : Set (UniformSpace β)} (h : uus, UniformAddGroup β) :
      theorem uniformGroup_sInf {β : Type u_2} [Group β] {us : Set (UniformSpace β)} (h : uus, UniformGroup β) :
      theorem uniformAddGroup_iInf {β : Type u_2} [AddGroup β] {ι : Sort u_3} {us' : ιUniformSpace β} (h' : ∀ (i : ι), UniformAddGroup β) :
      theorem uniformGroup_iInf {β : Type u_2} [Group β] {ι : Sort u_3} {us' : ιUniformSpace β} (h' : ∀ (i : ι), UniformGroup β) :
      theorem uniformAddGroup_inf {β : Type u_2} [AddGroup β] {u₁ : UniformSpace β} {u₂ : UniformSpace β} (h₁ : UniformAddGroup β) (h₂ : UniformAddGroup β) :
      theorem uniformGroup_inf {β : Type u_2} [Group β] {u₁ : UniformSpace β} {u₂ : UniformSpace β} (h₁ : UniformGroup β) (h₂ : UniformGroup β) :
      theorem UniformInducing.uniformAddGroup {β : Type u_2} [AddGroup β] {γ : Type u_3} [AddGroup γ] [UniformSpace γ] [UniformAddGroup γ] [UniformSpace β] {F : Type u_4} [FunLike F β γ] [AddMonoidHomClass F β γ] (f : F) (hf : UniformInducing f) :
      theorem UniformInducing.uniformGroup {β : Type u_2} [Group β] {γ : Type u_3} [Group γ] [UniformSpace γ] [UniformGroup γ] [UniformSpace β] {F : Type u_4} [FunLike F β γ] [MonoidHomClass F β γ] (f : F) (hf : UniformInducing f) :
      theorem UniformAddGroup.comap {β : Type u_2} [AddGroup β] {γ : Type u_3} [AddGroup γ] {u : UniformSpace γ} [UniformAddGroup γ] {F : Type u_4} [FunLike F β γ] [AddMonoidHomClass F β γ] (f : F) :
      theorem UniformGroup.comap {β : Type u_2} [Group β] {γ : Type u_3} [Group γ] {u : UniformSpace γ} [UniformGroup γ] {F : Type u_4} [FunLike F β γ] [MonoidHomClass F β γ] (f : F) :
      Equations
      • =
      instance Subgroup.uniformGroup {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] (S : Subgroup α) :
      Equations
      • =
      theorem uniformity_eq_comap_nhds_zero (α : Type u_1) [UniformSpace α] [AddGroup α] [UniformAddGroup α] :
      uniformity α = Filter.comap (fun (x : α × α) => x.2 - x.1) (nhds 0)
      theorem uniformity_eq_comap_nhds_one (α : Type u_1) [UniformSpace α] [Group α] [UniformGroup α] :
      uniformity α = Filter.comap (fun (x : α × α) => x.2 / x.1) (nhds 1)
      theorem uniformity_eq_comap_nhds_zero_swapped (α : Type u_1) [UniformSpace α] [AddGroup α] [UniformAddGroup α] :
      uniformity α = Filter.comap (fun (x : α × α) => x.1 - x.2) (nhds 0)
      theorem uniformity_eq_comap_nhds_one_swapped (α : Type u_1) [UniformSpace α] [Group α] [UniformGroup α] :
      uniformity α = Filter.comap (fun (x : α × α) => x.1 / x.2) (nhds 1)
      theorem UniformAddGroup.ext {G : Type u_3} [AddGroup G] {u : UniformSpace G} {v : UniformSpace G} (hu : UniformAddGroup G) (hv : UniformAddGroup G) (h : nhds 0 = nhds 0) :
      u = v
      theorem UniformGroup.ext {G : Type u_3} [Group G] {u : UniformSpace G} {v : UniformSpace G} (hu : UniformGroup G) (hv : UniformGroup G) (h : nhds 1 = nhds 1) :
      u = v
      theorem UniformAddGroup.ext_iff {G : Type u_3} [AddGroup G] {u : UniformSpace G} {v : UniformSpace G} (hu : UniformAddGroup G) (hv : UniformAddGroup G) :
      u = v nhds 0 = nhds 0
      theorem UniformGroup.ext_iff {G : Type u_3} [Group G] {u : UniformSpace G} {v : UniformSpace G} (hu : UniformGroup G) (hv : UniformGroup G) :
      u = v nhds 1 = nhds 1
      theorem UniformAddGroup.uniformity_countably_generated {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] [(nhds 0).IsCountablyGenerated] :
      (uniformity α).IsCountablyGenerated
      theorem UniformGroup.uniformity_countably_generated {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] [(nhds 1).IsCountablyGenerated] :
      (uniformity α).IsCountablyGenerated
      theorem uniformity_eq_comap_neg_add_nhds_zero {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] :
      uniformity α = Filter.comap (fun (x : α × α) => -x.1 + x.2) (nhds 0)
      theorem uniformity_eq_comap_inv_mul_nhds_one {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] :
      uniformity α = Filter.comap (fun (x : α × α) => x.1⁻¹ * x.2) (nhds 1)
      theorem uniformity_eq_comap_neg_add_nhds_zero_swapped {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] :
      uniformity α = Filter.comap (fun (x : α × α) => -x.2 + x.1) (nhds 0)
      theorem uniformity_eq_comap_inv_mul_nhds_one_swapped {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] :
      uniformity α = Filter.comap (fun (x : α × α) => x.2⁻¹ * x.1) (nhds 1)
      theorem Filter.HasBasis.uniformity_of_nhds_zero {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {ι : 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 {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] {ι : 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 {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {ι : 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 {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] {ι : 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 α] [UniformAddGroup α] {ι : 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 α] [UniformGroup α] {ι : 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_swapped {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {ι : 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_swapped {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] {ι : 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 uniformContinuous_of_tendsto_zero {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {hom : Type u_3} [UniformSpace β] [AddGroup β] [UniformAddGroup β] [FunLike hom α β] [AddMonoidHomClass hom α β] {f : hom} (h : Filter.Tendsto (⇑f) (nhds 0) (nhds 0)) :
      theorem uniformContinuous_of_tendsto_one {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] {hom : Type u_3} [UniformSpace β] [Group β] [UniformGroup β] [FunLike hom α β] [MonoidHomClass hom α β] {f : hom} (h : Filter.Tendsto (⇑f) (nhds 1) (nhds 1)) :
      theorem uniformContinuous_of_continuousAt_zero {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {hom : Type u_3} [UniformSpace β] [AddGroup β] [UniformAddGroup β] [FunLike hom α β] [AddMonoidHomClass hom α β] (f : hom) (hf : ContinuousAt (⇑f) 0) :

      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 uniformContinuous_of_continuousAt_one {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] {hom : Type u_3} [UniformSpace β] [Group β] [UniformGroup β] [FunLike hom α β] [MonoidHomClass hom α β] (f : hom) (hf : ContinuousAt (⇑f) 1) :

      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 MonoidHom.uniformContinuous_of_continuousAt_one {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] [UniformSpace β] [Group β] [UniformGroup β] (f : α →* β) (hf : ContinuousAt (⇑f) 1) :
      theorem UniformAddGroup.uniformContinuous_iff_open_ker {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {hom : Type u_3} [UniformSpace β] [DiscreteTopology β] [AddGroup β] [UniformAddGroup β] [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 UniformGroup.uniformContinuous_iff_open_ker {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] {hom : Type u_3} [UniformSpace β] [DiscreteTopology β] [Group β] [UniformGroup β] [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 uniformContinuous_addMonoidHom_of_continuous {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {hom : Type u_3} [UniformSpace β] [AddGroup β] [UniformAddGroup β] [FunLike hom α β] [AddMonoidHomClass hom α β] {f : hom} (h : Continuous f) :
      theorem uniformContinuous_monoidHom_of_continuous {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] {hom : Type u_3} [UniformSpace β] [Group β] [UniformGroup β] [FunLike hom α β] [MonoidHomClass hom α β] {f : hom} (h : Continuous f) :
      theorem CauchySeq.add {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {ι : Type u_3} [Preorder ι] {u : ια} {v : ια} (hu : CauchySeq u) (hv : CauchySeq v) :
      CauchySeq (u + v)
      theorem CauchySeq.mul {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] {ι : Type u_3} [Preorder ι] {u : ια} {v : ια} (hu : CauchySeq u) (hv : CauchySeq v) :
      CauchySeq (u * v)
      theorem CauchySeq.add_const {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {ι : Type u_3} [Preorder ι] {u : ια} {x : α} (hu : CauchySeq u) :
      CauchySeq fun (n : ι) => u n + x
      theorem CauchySeq.mul_const {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] {ι : Type u_3} [Preorder ι] {u : ια} {x : α} (hu : CauchySeq u) :
      CauchySeq fun (n : ι) => u n * x
      theorem CauchySeq.const_add {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {ι : Type u_3} [Preorder ι] {u : ια} {x : α} (hu : CauchySeq u) :
      CauchySeq fun (n : ι) => x + u n
      theorem CauchySeq.const_mul {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] {ι : Type u_3} [Preorder ι] {u : ια} {x : α} (hu : CauchySeq u) :
      CauchySeq fun (n : ι) => x * u n
      theorem CauchySeq.neg {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {ι : Type u_3} [Preorder ι] {u : ια} (h : CauchySeq u) :
      theorem CauchySeq.inv {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] {ι : Type u_3} [Preorder ι] {u : ια} (h : CauchySeq u) :
      theorem totallyBounded_iff_subset_finite_iUnion_nhds_zero {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {s : Set α} :
      TotallyBounded s Unhds 0, ∃ (t : Set α), t.Finite s yt, y +ᵥ U
      theorem totallyBounded_iff_subset_finite_iUnion_nhds_one {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] {s : Set α} :
      TotallyBounded s Unhds 1, ∃ (t : Set α), t.Finite s yt, y U
      theorem TendstoUniformlyOnFilter.add {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {ι : Type u_3} {l : Filter ι} {l' : Filter β} {f : ιβα} {f' : ιβα} {g : βα} {g' : βα} (hf : TendstoUniformlyOnFilter f g l l') (hf' : TendstoUniformlyOnFilter f' g' l l') :
      TendstoUniformlyOnFilter (f + f') (g + g') l l'
      theorem TendstoUniformlyOnFilter.mul {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] {ι : Type u_3} {l : Filter ι} {l' : Filter β} {f : ιβα} {f' : ιβα} {g : βα} {g' : βα} (hf : TendstoUniformlyOnFilter f g l l') (hf' : TendstoUniformlyOnFilter f' g' l l') :
      TendstoUniformlyOnFilter (f * f') (g * g') l l'
      theorem TendstoUniformlyOnFilter.sub {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {ι : Type u_3} {l : Filter ι} {l' : Filter β} {f : ιβα} {f' : ιβα} {g : βα} {g' : βα} (hf : TendstoUniformlyOnFilter f g l l') (hf' : TendstoUniformlyOnFilter f' g' l l') :
      TendstoUniformlyOnFilter (f - f') (g - g') l l'
      theorem TendstoUniformlyOnFilter.div {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] {ι : Type u_3} {l : Filter ι} {l' : Filter β} {f : ιβα} {f' : ιβα} {g : βα} {g' : βα} (hf : TendstoUniformlyOnFilter f g l l') (hf' : TendstoUniformlyOnFilter f' g' l l') :
      TendstoUniformlyOnFilter (f / f') (g / g') l l'
      theorem TendstoUniformlyOn.add {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {ι : Type u_3} {l : Filter ι} {f : ιβα} {f' : ιβα} {g : βα} {g' : βα} {s : Set β} (hf : TendstoUniformlyOn f g l s) (hf' : TendstoUniformlyOn f' g' l s) :
      TendstoUniformlyOn (f + f') (g + g') l s
      theorem TendstoUniformlyOn.mul {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] {ι : Type u_3} {l : Filter ι} {f : ιβα} {f' : ιβα} {g : βα} {g' : βα} {s : Set β} (hf : TendstoUniformlyOn f g l s) (hf' : TendstoUniformlyOn f' g' l s) :
      TendstoUniformlyOn (f * f') (g * g') l s
      theorem TendstoUniformlyOn.sub {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {ι : Type u_3} {l : Filter ι} {f : ιβα} {f' : ιβα} {g : βα} {g' : βα} {s : Set β} (hf : TendstoUniformlyOn f g l s) (hf' : TendstoUniformlyOn f' g' l s) :
      TendstoUniformlyOn (f - f') (g - g') l s
      theorem TendstoUniformlyOn.div {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] {ι : Type u_3} {l : Filter ι} {f : ιβα} {f' : ιβα} {g : βα} {g' : βα} {s : Set β} (hf : TendstoUniformlyOn f g l s) (hf' : TendstoUniformlyOn f' g' l s) :
      TendstoUniformlyOn (f / f') (g / g') l s
      theorem TendstoUniformly.add {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {ι : Type u_3} {l : Filter ι} {f : ιβα} {f' : ιβα} {g : βα} {g' : βα} (hf : TendstoUniformly f g l) (hf' : TendstoUniformly f' g' l) :
      TendstoUniformly (f + f') (g + g') l
      theorem TendstoUniformly.mul {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] {ι : Type u_3} {l : Filter ι} {f : ιβα} {f' : ιβα} {g : βα} {g' : βα} (hf : TendstoUniformly f g l) (hf' : TendstoUniformly f' g' l) :
      TendstoUniformly (f * f') (g * g') l
      theorem TendstoUniformly.sub {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {ι : Type u_3} {l : Filter ι} {f : ιβα} {f' : ιβα} {g : βα} {g' : βα} (hf : TendstoUniformly f g l) (hf' : TendstoUniformly f' g' l) :
      TendstoUniformly (f - f') (g - g') l
      theorem TendstoUniformly.div {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] {ι : Type u_3} {l : Filter ι} {f : ιβα} {f' : ιβα} {g : βα} {g' : βα} (hf : TendstoUniformly f g l) (hf' : TendstoUniformly f' g' l) :
      TendstoUniformly (f / f') (g / g') l
      theorem UniformCauchySeqOn.add {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {ι : Type u_3} {l : Filter ι} {f : ιβα} {f' : ιβα} {s : Set β} (hf : UniformCauchySeqOn f l s) (hf' : UniformCauchySeqOn f' l s) :
      theorem UniformCauchySeqOn.mul {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] {ι : Type u_3} {l : Filter ι} {f : ιβα} {f' : ιβα} {s : Set β} (hf : UniformCauchySeqOn f l s) (hf' : UniformCauchySeqOn f' l s) :
      theorem UniformCauchySeqOn.sub {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {ι : Type u_3} {l : Filter ι} {f : ιβα} {f' : ιβα} {s : Set β} (hf : UniformCauchySeqOn f l s) (hf' : UniformCauchySeqOn f' l s) :
      theorem UniformCauchySeqOn.div {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] {ι : Type u_3} {l : Filter ι} {f : ιβα} {f' : ιβα} {s : Set β} (hf : UniformCauchySeqOn f l s) (hf' : UniformCauchySeqOn f' l s) :
      theorem TopologicalAddGroup.toUniformSpace.proof_1 (G : Type u_1) [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] :
      Filter.Tendsto Prod.swap (Filter.comap (fun (p : G × G) => p.2 - p.1) (nhds 0)) (Filter.comap (fun (p : G × G) => p.2 - p.1) (nhds 0))
      theorem TopologicalAddGroup.toUniformSpace.proof_3 (G : Type u_1) [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] :
      ∀ (x : G), nhds x = Filter.comap (Prod.mk x) (Filter.comap (fun (p : G × G) => p.2 - p.1) (nhds 0))
      theorem TopologicalAddGroup.toUniformSpace.proof_2 (G : Type u_1) [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] :
      ((Filter.comap (fun (p : G × G) => p.2 - p.1) (nhds 0)).lift' fun (s : Set (G × G)) => compRel s s) Filter.comap (fun (p : G × G) => p.2 - p.1) (nhds 0)

      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 UniformAddGroup 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
      Instances For

        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 UniformGroup 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
        Instances For
          theorem uniformity_eq_comap_nhds_one' (G : Type u_1) [Group G] [TopologicalSpace G] [TopologicalGroup G] :
          uniformity G = Filter.comap (fun (p : G × G) => p.2 / p.1) (nhds 1)
          Equations
          • =
          theorem AddMonoidHom.tendsto_coe_cofinite_of_discrete {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [T2Space G] {H : Type u_2} [AddGroup H] {f : H →+ G} (hf : Function.Injective f) (hf' : DiscreteTopology f.range) :
          Filter.Tendsto (⇑f) Filter.cofinite (Filter.cocompact G)
          theorem MonoidHom.tendsto_coe_cofinite_of_discrete {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] [T2Space G] {H : Type u_2} [Group H] {f : H →* G} (hf : Function.Injective f) (hf' : DiscreteTopology f.range) :
          Filter.Tendsto (⇑f) Filter.cofinite (Filter.cocompact G)
          theorem TopologicalAddGroup.tendstoUniformly_iff {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] {ι : Type u_2} {α : Type u_3} (F : ιαG) (f : αG) (p : Filter ι) :
          TendstoUniformly F f p unhds 0, ∀ᶠ (i : ι) in p, ∀ (a : α), F i a - f a u
          theorem TopologicalGroup.tendstoUniformly_iff {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] {ι : Type u_2} {α : Type u_3} (F : ιαG) (f : αG) (p : Filter ι) :
          TendstoUniformly F f p unhds 1, ∀ᶠ (i : ι) in p, ∀ (a : α), F i a / f a u
          theorem TopologicalAddGroup.tendstoUniformlyOn_iff {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] {ι : Type u_2} {α : Type u_3} (F : ιαG) (f : αG) (p : Filter ι) (s : Set α) :
          TendstoUniformlyOn F f p s unhds 0, ∀ᶠ (i : ι) in p, as, F i a - f a u
          theorem TopologicalGroup.tendstoUniformlyOn_iff {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] {ι : Type u_2} {α : Type u_3} (F : ιαG) (f : αG) (p : Filter ι) (s : Set α) :
          TendstoUniformlyOn F f p s unhds 1, ∀ᶠ (i : ι) in p, as, F i a / f a u
          theorem TopologicalAddGroup.tendstoLocallyUniformly_iff {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] {ι : Type u_2} {α : Type u_3} [TopologicalSpace α] (F : ιαG) (f : αG) (p : Filter ι) :
          TendstoLocallyUniformly F f p unhds 0, ∀ (x : α), tnhds x, ∀ᶠ (i : ι) in p, at, F i a - f a u
          theorem TopologicalGroup.tendstoLocallyUniformly_iff {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] {ι : Type u_2} {α : Type u_3} [TopologicalSpace α] (F : ιαG) (f : αG) (p : Filter ι) :
          TendstoLocallyUniformly F f p unhds 1, ∀ (x : α), tnhds x, ∀ᶠ (i : ι) in p, at, F i a / f a u
          theorem TopologicalAddGroup.tendstoLocallyUniformlyOn_iff {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] {ι : Type u_2} {α : Type u_3} [TopologicalSpace α] (F : ιαG) (f : αG) (p : Filter ι) (s : Set α) :
          TendstoLocallyUniformlyOn F f p s unhds 0, xs, tnhdsWithin x s, ∀ᶠ (i : ι) in p, at, F i a - f a u
          theorem TopologicalGroup.tendstoLocallyUniformlyOn_iff {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] {ι : Type u_2} {α : Type u_3} [TopologicalSpace α] (F : ιαG) (f : αG) (p : Filter ι) (s : Set α) :
          TendstoLocallyUniformlyOn F f p s unhds 1, xs, tnhdsWithin x s, ∀ᶠ (i : ι) in p, at, F i a / f a u
          theorem tendsto_sub_comap_self {α : Type u_1} {β : Type u_2} {hom : Type u_3} [TopologicalSpace α] [AddGroup α] [TopologicalAddGroup α] [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)
          theorem tendsto_div_comap_self {α : Type u_1} {β : Type u_2} {hom : Type u_3} [TopologicalSpace α] [Group α] [TopologicalGroup α] [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 IsDenseInducing.extend_Z_bilin {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {G : Type u_5} [TopologicalSpace α] [AddCommGroup α] [TopologicalAddGroup α] [TopologicalSpace β] [AddCommGroup β] [TopologicalSpace γ] [AddCommGroup γ] [TopologicalAddGroup γ] [TopologicalSpace δ] [AddCommGroup δ] [UniformSpace G] [AddCommGroup G] {e : β →+ α} (de : IsDenseInducing e) {f : δ →+ γ} (df : IsDenseInducing f) {φ : β →+ δ →+ G} (hφ : Continuous fun (p : β × δ) => (φ p.1) p.2) [UniformAddGroup G] [T0Space G] [CompleteSpace G] :
          Continuous (.extend fun (p : β × δ) => (φ p.1) p.2)

          Bourbaki GT III.6.5 Theorem I: ℤ-bilinear continuous maps from dense images into a complete Hausdorff group extend by continuity. Note: Bourbaki assumes that α and β are also complete Hausdorff, but this is not necessary.

          The quotient G ⧸ N of a complete first countable topological additive group G by a normal additive subgroup is itself complete. Consequently, quotients of Banach spaces by subspaces are complete. [N. Bourbaki, General Topology, IX.3.1 Proposition 4][bourbaki1966b]

          Because an additive topological group is not equipped with a UniformSpace instance by default, we must explicitly provide it in order to consider completeness. See QuotientAddGroup.completeSpace for a version in which G is already equipped with a uniform structure.

          Equations
          • =

          The quotient G ⧸ N of a complete first countable topological group G by a normal subgroup is itself complete. [N. Bourbaki, General Topology, IX.3.1 Proposition 4][bourbaki1966b]

          Because a topological group is not equipped with a UniformSpace instance by default, we must explicitly provide it in order to consider completeness. See QuotientGroup.completeSpace for a version in which G is already equipped with a uniform structure.

          Equations
          • =

          The quotient G ⧸ N of a complete first countable uniform additive group G by a normal additive subgroup is itself complete. Consequently, quotients of Banach spaces by subspaces are complete. In contrast to QuotientAddGroup.completeSpace', in this version G is already equipped with a uniform structure. [N. Bourbaki, General Topology, IX.3.1 Proposition 4][bourbaki1966b]

          Even though G is equipped with a uniform structure, the quotient G ⧸ N does not inherit a uniform structure, so it is still provided manually via TopologicalAddGroup.toUniformSpace. In the most common use case ─ quotients of normed additive commutative groups by subgroups ─ significant care was taken so that the uniform structure inherent in that setting coincides (definitionally) with the uniform structure provided here.

          Equations
          • =
          instance QuotientGroup.completeSpace (G : Type u) [Group G] [us : UniformSpace G] [UniformGroup G] [FirstCountableTopology G] (N : Subgroup G) [N.Normal] [hG : CompleteSpace G] :

          The quotient G ⧸ N of a complete first countable uniform group G by a normal subgroup is itself complete. In contrast to QuotientGroup.completeSpace', in this version G is already equipped with a uniform structure. [N. Bourbaki, General Topology, IX.3.1 Proposition 4][bourbaki1966b]

          Even though G is equipped with a uniform structure, the quotient G ⧸ N does not inherit a uniform structure, so it is still provided manually via TopologicalGroup.toUniformSpace. In the most common use cases, this coincides (definitionally) with the uniform structure on the quotient obtained via other means.

          Equations
          • =