Documentation

Mathlib.Topology.Algebra.UniformGroup.Defs

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 #

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

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

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

Instances
    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 UniformGroup.mk' {α : Type u_3} [UniformSpace α] [Group α] (h₁ : UniformContinuous fun (p : α × α) => p.1 * p.2) (h₂ : UniformContinuous fun (p : α) => p⁻¹) :
      theorem UniformAddGroup.mk' {α : Type u_3} [UniformSpace α] [AddGroup α] (h₁ : UniformContinuous fun (p : α × α) => p.1 + p.2) (h₂ : UniformContinuous fun (p : α) => -p) :
      theorem uniformContinuous_div {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] :
      UniformContinuous fun (p : α × α) => p.1 / p.2
      theorem uniformContinuous_sub {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] :
      UniformContinuous fun (p : α × α) => p.1 - p.2
      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.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.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} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] [UniformSpace β] {f : βα} (hf : UniformContinuous f) :
      UniformContinuous fun (x : β) => -f x
      theorem uniformContinuous_inv {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] :
      UniformContinuous fun (x : α) => x⁻¹
      theorem uniformContinuous_neg {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] :
      UniformContinuous fun (x : α) => -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} {β : 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} [UniformSpace α] [Group α] [UniformGroup α] :
      UniformContinuous fun (p : α × α) => p.1 * p.2
      theorem uniformContinuous_add {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] :
      UniformContinuous fun (p : α × α) => p.1 + p.2
      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.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.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.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_mul_left {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] (a : α) :
      UniformContinuous fun (b : α) => a * b
      theorem uniformContinuous_add_left {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] (a : α) :
      UniformContinuous fun (b : α) => a + b
      theorem uniformContinuous_mul_right {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] (a : α) :
      UniformContinuous fun (b : α) => b * a
      theorem uniformContinuous_add_right {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] (a : α) :
      UniformContinuous fun (b : α) => b + 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} {β : 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} [UniformSpace α] [Group α] [UniformGroup α] (a : α) :
      UniformContinuous fun (b : α) => b / a
      theorem uniformContinuous_sub_const {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] (a : α) :
      UniformContinuous fun (b : α) => b - a
      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} {β : 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} [UniformSpace α] [Group α] [UniformGroup α] (n : ) :
      UniformContinuous fun (x : α) => x ^ n
      theorem uniformContinuous_const_nsmul {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] (n : ) :
      UniformContinuous fun (x : α) => n 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} {β : 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} [UniformSpace α] [Group α] [UniformGroup α] (n : ) :
      UniformContinuous fun (x : α) => x ^ n
      theorem uniformContinuous_const_zsmul {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] (n : ) :
      UniformContinuous fun (x : α) => n x
      theorem instUniformGroupProd {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] [UniformSpace β] [Group β] [UniformGroup β] :
      theorem uniformity_translate_mul {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] (a : α) :
      Filter.map (fun (x : α × α) => (x.1 * a, x.2 * a)) (uniformity α) = uniformity α
      theorem uniformity_translate_add {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] (a : α) :
      Filter.map (fun (x : α × α) => (x.1 + a, x.2 + a)) (uniformity α) = uniformity α
      theorem uniformGroup_sInf {β : Type u_2} [Group β] {us : Set (UniformSpace β)} (h : uus, UniformGroup β) :
      theorem uniformAddGroup_sInf {β : Type u_2} [AddGroup β] {us : Set (UniformSpace β)} (h : uus, UniformAddGroup β) :
      theorem uniformGroup_iInf {β : Type u_2} [Group β] {ι : Sort u_3} {us' : ιUniformSpace β} (h' : ∀ (i : ι), UniformGroup β) :
      theorem uniformAddGroup_iInf {β : Type u_2} [AddGroup β] {ι : Sort u_3} {us' : ιUniformSpace β} (h' : ∀ (i : ι), UniformAddGroup β) :
      theorem uniformGroup_inf {β : Type u_2} [Group β] {u₁ u₂ : UniformSpace β} (h₁ : UniformGroup β) (h₂ : UniformGroup β) :
      theorem uniformAddGroup_inf {β : Type u_2} [AddGroup β] {u₁ u₂ : UniformSpace β} (h₁ : UniformAddGroup β) (h₂ : UniformAddGroup β) :
      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 (α : Type u_1) [UniformSpace α] [AddGroup α] [UniformAddGroup α] :
      uniformity α = Filter.comap (fun (x : α × α) => x.2 - x.1) (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 uniformity_eq_comap_nhds_zero_swapped (α : Type u_1) [UniformSpace α] [AddGroup α] [UniformAddGroup α] :
      uniformity α = Filter.comap (fun (x : α × α) => x.1 - x.2) (nhds 0)
      theorem UniformGroup.ext {G : Type u_3} [Group G] {u v : UniformSpace G} (hu : UniformGroup G) (hv : UniformGroup G) (h : nhds 1 = nhds 1) :
      u = v
      theorem UniformAddGroup.ext {G : Type u_3} [AddGroup G] {u v : UniformSpace G} (hu : UniformAddGroup G) (hv : UniformAddGroup G) (h : nhds 0 = nhds 0) :
      u = v
      theorem UniformGroup.ext_iff {G : Type u_3} [Group G] {u v : UniformSpace G} (hu : UniformGroup G) (hv : UniformGroup G) :
      u = v nhds 1 = nhds 1
      theorem UniformAddGroup.ext_iff {G : Type u_3} [AddGroup G] {u v : UniformSpace G} (hu : UniformAddGroup G) (hv : UniformAddGroup G) :
      u = v nhds 0 = nhds 0
      theorem UniformGroup.uniformity_countably_generated {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] [(nhds 1).IsCountablyGenerated] :
      (uniformity α).IsCountablyGenerated
      theorem UniformAddGroup.uniformity_countably_generated {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] [(nhds 0).IsCountablyGenerated] :
      (uniformity α).IsCountablyGenerated
      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 {α : 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_swapped {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] :
      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 α] [UniformAddGroup α] :
      uniformity α = Filter.comap (fun (x : α × α) => -x.2 + x.1) (nhds 0)
      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 {α : 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 {α : 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 {α : 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_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_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 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 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_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_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 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 MonoidHom.uniformContinuous_of_continuousAt_one {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] [UniformSpace β] [Group β] [UniformGroup β] (f : α →* β) (hf : ContinuousAt (⇑f) 1) :
      theorem UniformGroup.uniformContinuous_iff_isOpen_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 UniformAddGroup.uniformContinuous_iff_isOpen_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.

      @[deprecated UniformGroup.uniformContinuous_iff_isOpen_ker]
      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

      Alias of UniformGroup.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 UniformAddGroup.uniformContinuous_iff_isOpen_ker]
      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

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

      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 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) :

      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

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