Documentation

Mathlib.Topology.Algebra.IsUniformGroup.Defs

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 #

Main results #

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

structure IsUniformGroup (α : Type u_3) [UniformSpace α] [Group α] :

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

Instances For
    @[deprecated IsUniformGroup (since := "2025-03-26")]
    def UniformGroup (α : Type u_3) [UniformSpace α] [Group α] :

    Alias of IsUniformGroup.


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

    Equations
    Instances For
      structure IsUniformAddGroup (α : Type u_3) [UniformSpace α] [AddGroup α] :

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

      Instances For
        @[deprecated IsUniformAddGroup (since := "2025-03-26")]
        def UniformAddGroup (α : Type u_3) [UniformSpace α] [AddGroup α] :

        Alias of IsUniformAddGroup.


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

        Equations
        Instances For
          theorem IsUniformGroup.mk' {α : Type u_3} [UniformSpace α] [Group α] (h₁ : UniformContinuous fun (p : Prod α α) => HMul.hMul p.fst p.snd) (h₂ : UniformContinuous fun (p : α) => Inv.inv p) :
          theorem IsUniformAddGroup.mk' {α : Type u_3} [UniformSpace α] [AddGroup α] (h₁ : UniformContinuous fun (p : Prod α α) => HAdd.hAdd p.fst p.snd) (h₂ : UniformContinuous fun (p : α) => Neg.neg p) :
          theorem uniformContinuous_div {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] :
          UniformContinuous fun (p : Prod α α) => HDiv.hDiv p.fst p.snd
          theorem UniformContinuous.div {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] [UniformSpace β] {f g : βα} (hf : UniformContinuous f) (hg : UniformContinuous g) :
          UniformContinuous fun (x : β) => HDiv.hDiv (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 : β) => HSub.hSub (f x) (g x)
          theorem UniformContinuous.inv {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] [UniformSpace β] {f : βα} (hf : UniformContinuous f) :
          UniformContinuous fun (x : β) => Inv.inv (f x)
          theorem UniformContinuous.neg {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] [UniformSpace β] {f : βα} (hf : UniformContinuous f) :
          UniformContinuous fun (x : β) => Neg.neg (f x)
          theorem uniformContinuous_inv {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] :
          UniformContinuous fun (x : α) => Inv.inv 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 : β) => HMul.hMul (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 : β) => HAdd.hAdd (f x) (g x)
          theorem uniformContinuous_mul {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] :
          UniformContinuous fun (p : Prod α α) => HMul.hMul p.fst p.snd
          theorem UniformContinuous.mul_const {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] [UniformSpace β] {f : βα} (hf : UniformContinuous f) (a : α) :
          UniformContinuous fun (x : β) => HMul.hMul (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 : β) => HAdd.hAdd (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 : β) => HMul.hMul 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 : β) => HAdd.hAdd a (f x)
          theorem uniformContinuous_mul_left {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] (a : α) :
          UniformContinuous fun (b : α) => HMul.hMul a b
          theorem uniformContinuous_add_left {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] (a : α) :
          UniformContinuous fun (b : α) => HAdd.hAdd a b
          theorem uniformContinuous_mul_right {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] (a : α) :
          UniformContinuous fun (b : α) => HMul.hMul b a
          theorem uniformContinuous_add_right {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] (a : α) :
          UniformContinuous fun (b : α) => HAdd.hAdd b a
          theorem UniformContinuous.div_const {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] [UniformSpace β] {f : βα} (hf : UniformContinuous f) (a : α) :
          UniformContinuous fun (x : β) => HDiv.hDiv (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 : β) => HSub.hSub (f x) a
          theorem uniformContinuous_div_const {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] (a : α) :
          UniformContinuous fun (b : α) => HDiv.hDiv b a
          theorem uniformContinuous_sub_const {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] (a : α) :
          UniformContinuous fun (b : α) => HSub.hSub b a
          theorem UniformContinuous.pow_const {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] [UniformSpace β] {f : βα} (hf : UniformContinuous f) (n : Nat) :
          UniformContinuous fun (x : β) => HPow.hPow (f x) n
          theorem UniformContinuous.const_nsmul {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] [UniformSpace β] {f : βα} (hf : UniformContinuous f) (n : Nat) :
          UniformContinuous fun (x : β) => HSMul.hSMul n (f x)
          theorem uniformContinuous_pow_const {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] (n : Nat) :
          UniformContinuous fun (x : α) => HPow.hPow x n
          theorem UniformContinuous.zpow_const {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] [UniformSpace β] {f : βα} (hf : UniformContinuous f) (n : Int) :
          UniformContinuous fun (x : β) => HPow.hPow (f x) n
          theorem UniformContinuous.const_zsmul {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] [UniformSpace β] {f : βα} (hf : UniformContinuous f) (n : Int) :
          UniformContinuous fun (x : β) => HSMul.hSMul n (f x)
          theorem uniformContinuous_zpow_const {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] (n : Int) :
          UniformContinuous fun (x : α) => HPow.hPow x n
          @[deprecated IsUniformAddGroup.to_topologicalAddGroup (since := "2025-03-31")]

          Alias of IsUniformAddGroup.to_topologicalAddGroup.

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

          Alias of IsUniformGroup.to_topologicalGroup.

          theorem Prod.instIsUniformGroup {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] [UniformSpace β] [Group β] [IsUniformGroup β] :
          @[deprecated Prod.instIsUniformAddGroup (since := "2025-03-31")]

          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 β] :

          Alias of Prod.instIsUniformGroup.

          theorem uniformity_translate_mul {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] (a : α) :
          Eq (Filter.map (fun (x : Prod α α) => { fst := HMul.hMul x.fst a, snd := HMul.hMul x.snd a }) (uniformity α)) (uniformity α)
          theorem uniformity_translate_add {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] (a : α) :
          Eq (Filter.map (fun (x : Prod α α) => { fst := HAdd.hAdd x.fst a, snd := HAdd.hAdd x.snd a }) (uniformity α)) (uniformity α)
          theorem isUniformGroup_sInf {β : Type u_2} [Group β] {us : Set (UniformSpace β)} (h : ∀ (u : UniformSpace β), Membership.mem us uIsUniformGroup β) :
          theorem isUniformAddGroup_sInf {β : Type u_2} [AddGroup β] {us : Set (UniformSpace β)} (h : ∀ (u : UniformSpace β), Membership.mem us uIsUniformAddGroup β) :
          @[deprecated isUniformAddGroup_sInf (since := "2025-03-31")]
          theorem uniformAddGroup_sInf {β : Type u_2} [AddGroup β] {us : Set (UniformSpace β)} (h : ∀ (u : UniformSpace β), Membership.mem us uIsUniformAddGroup β) :

          Alias of isUniformAddGroup_sInf.

          @[deprecated isUniformGroup_sInf (since := "2025-03-31")]
          theorem uniformGroup_sInf {β : Type u_2} [Group β] {us : Set (UniformSpace β)} (h : ∀ (u : UniformSpace β), Membership.mem us uIsUniformGroup β) :

          Alias of isUniformGroup_sInf.

          theorem isUniformGroup_iInf {β : Type u_2} [Group β] {ι : Sort u_3} {us' : ιUniformSpace β} (h' : ∀ (i : ι), IsUniformGroup β) :
          theorem isUniformAddGroup_iInf {β : Type u_2} [AddGroup β] {ι : Sort u_3} {us' : ιUniformSpace β} (h' : ∀ (i : ι), IsUniformAddGroup β) :
          @[deprecated isUniformAddGroup_iInf (since := "2025-03-31")]
          theorem uniformAddGroup_iInf {β : Type u_2} [AddGroup β] {ι : Sort u_3} {us' : ιUniformSpace β} (h' : ∀ (i : ι), 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 β) :

          Alias of isUniformGroup_iInf.

          theorem isUniformGroup_inf {β : Type u_2} [Group β] {u₁ u₂ : UniformSpace β} (h₁ : IsUniformGroup β) (h₂ : IsUniformGroup β) :
          theorem isUniformAddGroup_inf {β : Type u_2} [AddGroup β] {u₁ u₂ : UniformSpace β} (h₁ : IsUniformAddGroup β) (h₂ : IsUniformAddGroup β) :
          @[deprecated isUniformAddGroup_inf (since := "2025-03-31")]
          theorem uniformAddGroup_inf {β : Type u_2} [AddGroup β] {u₁ u₂ : UniformSpace β} (h₁ : IsUniformAddGroup β) (h₂ : 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 β) :

          Alias of isUniformGroup_inf.

          theorem uniformity_eq_comap_nhds_one (α : Type u_1) [UniformSpace α] [Group α] [IsUniformGroup α] :
          Eq (uniformity α) (Filter.comap (fun (x : Prod α α) => HDiv.hDiv x.snd x.fst) (nhds 1))
          theorem uniformity_eq_comap_nhds_zero (α : Type u_1) [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] :
          Eq (uniformity α) (Filter.comap (fun (x : Prod α α) => HSub.hSub x.snd x.fst) (nhds 0))
          theorem uniformity_eq_comap_nhds_one_swapped (α : Type u_1) [UniformSpace α] [Group α] [IsUniformGroup α] :
          Eq (uniformity α) (Filter.comap (fun (x : Prod α α) => HDiv.hDiv x.fst x.snd) (nhds 1))
          theorem IsUniformGroup.ext {G : Type u_3} [Group G] {u v : UniformSpace G} (hu : IsUniformGroup G) (hv : IsUniformGroup G) (h : Eq (nhds 1) (nhds 1)) :
          Eq u v
          theorem IsUniformAddGroup.ext {G : Type u_3} [AddGroup G] {u v : UniformSpace G} (hu : IsUniformAddGroup G) (hv : IsUniformAddGroup G) (h : Eq (nhds 0) (nhds 0)) :
          Eq 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 : Eq (nhds 0) (nhds 0)) :
          Eq 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 : Eq (nhds 1) (nhds 1)) :
          Eq 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) :
          Iff (Eq u v) (Eq (nhds 1) (nhds 1))
          theorem IsUniformAddGroup.ext_iff {G : Type u_3} [AddGroup G] {u v : UniformSpace G} (hu : IsUniformAddGroup G) (hv : IsUniformAddGroup G) :
          Iff (Eq u v) (Eq (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) :
          Iff (Eq u v) (Eq (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) :
          Iff (Eq u v) (Eq (nhds 1) (nhds 1))

          Alias of IsUniformGroup.ext_iff.

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

          Alias of IsUniformAddGroup.uniformity_countably_generated.

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

          Alias of IsUniformGroup.uniformity_countably_generated.

          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 : ι) => setOf fun (x : Prod α α) => Membership.mem (U i) (HDiv.hDiv x.snd x.fst)
          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 : ι) => setOf fun (x : Prod α α) => Membership.mem (U i) (HSub.hSub x.snd x.fst)
          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 : ι) => setOf fun (x : Prod α α) => Membership.mem (U i) (HMul.hMul (Inv.inv x.fst) x.snd)
          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 : ι) => setOf fun (x : Prod α α) => Membership.mem (U i) (HAdd.hAdd (Neg.neg x.fst) x.snd)
          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 : ι) => setOf fun (x : Prod α α) => Membership.mem (U i) (HDiv.hDiv x.fst x.snd)
          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 : ι) => setOf fun (x : Prod α α) => Membership.mem (U i) (HSub.hSub x.fst x.snd)
          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 : ι) => setOf fun (x : Prod α α) => Membership.mem (U i) (HMul.hMul (Inv.inv x.snd) x.fst)
          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 : ι) => setOf fun (x : Prod α α) => Membership.mem (U i) (HAdd.hAdd (Neg.neg x.snd) x.fst)
          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 (DFunLike.coe f) (nhds 1) (nhds 1)) :
          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 (DFunLike.coe f) (nhds 0) (nhds 0)) :
          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 (DFunLike.coe 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 α] [IsUniformAddGroup α] {hom : Type u_3} [UniformSpace β] [AddGroup β] [IsUniformAddGroup β] [FunLike hom α β] [AddMonoidHomClass hom α β] (f : hom) (hf : ContinuousAt (DFunLike.coe 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.

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

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

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

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

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

          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 (DFunLike.coe 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 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
          • One or more equations did not get rendered due to their size.
          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 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
            • One or more equations did not get rendered due to their size.
            Instances For
              @[deprecated isUniformAddGroup_of_addCommGroup (since := "2025-02-28")]

              Alias of isUniformAddGroup_of_addCommGroup.

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

              Alias of isUniformGroup_of_commGroup.

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

              Alias of isUniformAddGroup_of_addCommGroup.

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

              Alias of isUniformGroup_of_commGroup.

              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 (DFunLike.coe e)) (x₀ : α) :
              Filter.Tendsto (fun (t : Prod β β) => HDiv.hDiv t.snd t.fst) (Filter.comap (fun (p : Prod β β) => { fst := DFunLike.coe e p.fst, snd := DFunLike.coe e p.snd }) (nhds { fst := x₀, snd := 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 (DFunLike.coe e)) (x₀ : α) :
              Filter.Tendsto (fun (t : Prod β β) => HSub.hSub t.snd t.fst) (Filter.comap (fun (p : Prod β β) => { fst := DFunLike.coe e p.fst, snd := DFunLike.coe e p.snd }) (nhds { fst := x₀, snd := x₀ })) (nhds 0)