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
    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.mk' {α : Type u_3} [UniformSpace α] [AddGroup α] (h₁ : UniformContinuous fun p => p.fst + p.snd) (h₂ : UniformContinuous fun p => -p) :
      theorem UniformGroup.mk' {α : Type u_3} [UniformSpace α] [Group α] (h₁ : UniformContinuous fun p => p.fst * p.snd) (h₂ : UniformContinuous fun p => p⁻¹) :
      theorem uniformContinuous_sub {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] :
      UniformContinuous fun p => p.fst - p.snd
      theorem uniformContinuous_div {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] :
      UniformContinuous fun p => p.fst / p.snd
      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.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.fst + p.snd
      theorem uniformContinuous_mul {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] :
      UniformContinuous fun p => p.fst * p.snd
      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
      abbrev UniformContinuous.const_nsmul.match_1 (motive : Prop) :
      (x : ) → (Unitmotive 0) → ((n : ) → motive (Nat.succ n)) → motive x
      Equations
      Instances For
        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_pow_const {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] (n : ) :
        UniformContinuous fun x => x ^ n
        abbrev UniformContinuous.const_zsmul.match_1 (motive : Prop) :
        (x : ) → ((n : ) → motive (Int.ofNat n)) → ((n : ) → motive (Int.negSucc n)) → motive x
        Equations
        Instances For
          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_zpow_const {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] (n : ) :
          UniformContinuous fun x => x ^ n
          theorem uniformity_translate_add {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] (a : α) :
          Filter.map (fun x => (x.fst + a, x.snd + a)) (uniformity α) = uniformity α
          theorem uniformity_translate_mul {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] (a : α) :
          Filter.map (fun x => (x.fst * a, x.snd * a)) (uniformity α) = uniformity α
          theorem uniformEmbedding_translate_add {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] (a : α) :
          UniformEmbedding fun x => x + a
          theorem uniformEmbedding_translate_mul {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] (a : α) :
          UniformEmbedding fun x => x * a
          theorem uniformAddGroup_sInf {β : Type u_2} [AddGroup β] {us : Set (UniformSpace β)} (h : ∀ (u : UniformSpace β), u usUniformAddGroup β) :
          theorem uniformGroup_sInf {β : Type u_2} [Group β] {us : Set (UniformSpace β)} (h : ∀ (u : UniformSpace β), u usUniformGroup β) :
          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 uniformAddGroup_comap {β : Type u_2} [AddGroup β] {γ : Type u_3} [AddGroup γ] {u : UniformSpace γ} [UniformAddGroup γ] {F : Type u_4} [AddMonoidHomClass F β γ] (f : F) :
          theorem uniformGroup_comap {β : Type u_2} [Group β] {γ : Type u_3} [Group γ] {u : UniformSpace γ} [UniformGroup γ] {F : Type u_4} [MonoidHomClass F β γ] (f : F) :
          theorem uniformity_eq_comap_nhds_zero (α : Type u_1) [UniformSpace α] [AddGroup α] [UniformAddGroup α] :
          uniformity α = Filter.comap (fun x => x.snd - x.fst) (nhds 0)
          theorem uniformity_eq_comap_nhds_one (α : Type u_1) [UniformSpace α] [Group α] [UniformGroup α] :
          uniformity α = Filter.comap (fun x => x.snd / x.fst) (nhds 1)
          theorem uniformity_eq_comap_nhds_zero_swapped (α : Type u_1) [UniformSpace α] [AddGroup α] [UniformAddGroup α] :
          uniformity α = Filter.comap (fun x => x.fst - x.snd) (nhds 0)
          theorem uniformity_eq_comap_nhds_one_swapped (α : Type u_1) [UniformSpace α] [Group α] [UniformGroup α] :
          uniformity α = Filter.comap (fun x => x.fst / x.snd) (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 uniformity_eq_comap_neg_add_nhds_zero {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] :
          uniformity α = Filter.comap (fun x => -x.fst + x.snd) (nhds 0)
          theorem uniformity_eq_comap_inv_mul_nhds_one {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] :
          uniformity α = Filter.comap (fun x => x.fst⁻¹ * x.snd) (nhds 1)
          theorem Filter.HasBasis.uniformity_of_nhds_zero {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {ι : Sort u_3} {p : ιProp} {U : ιSet α} (h : Filter.HasBasis (nhds 0) p U) :
          Filter.HasBasis (uniformity α) p fun i => {x | x.snd - x.fst U i}
          theorem Filter.HasBasis.uniformity_of_nhds_one {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] {ι : Sort u_3} {p : ιProp} {U : ιSet α} (h : Filter.HasBasis (nhds 1) p U) :
          Filter.HasBasis (uniformity α) p fun i => {x | x.snd / x.fst 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 : Filter.HasBasis (nhds 0) p U) :
          Filter.HasBasis (uniformity α) p fun i => {x | -x.fst + x.snd 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 : Filter.HasBasis (nhds 1) p U) :
          Filter.HasBasis (uniformity α) p fun i => {x | x.fst⁻¹ * x.snd U i}
          theorem Filter.HasBasis.uniformity_of_nhds_zero_swapped {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {ι : Sort u_3} {p : ιProp} {U : ιSet α} (h : Filter.HasBasis (nhds 0) p U) :
          Filter.HasBasis (uniformity α) p fun i => {x | x.fst - x.snd U i}
          theorem Filter.HasBasis.uniformity_of_nhds_one_swapped {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] {ι : Sort u_3} {p : ιProp} {U : ιSet α} (h : Filter.HasBasis (nhds 1) p U) :
          Filter.HasBasis (uniformity α) p fun i => {x | x.fst / x.snd 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 : Filter.HasBasis (nhds 0) p U) :
          Filter.HasBasis (uniformity α) p fun i => {x | -x.snd + x.fst 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 : Filter.HasBasis (nhds 1) p U) :
          Filter.HasBasis (uniformity α) p fun i => {x | x.snd⁻¹ * x.fst U i}
          theorem addGroup_separationRel {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] (x : α) (y : α) :
          (x, y) separationRel α x - y closure {0}
          theorem group_separationRel {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] (x : α) (y : α) :
          (x, y) separationRel α x / y closure {1}
          theorem uniformContinuous_of_tendsto_zero {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {hom : Type u_3} [UniformSpace β] [AddGroup β] [UniformAddGroup β] [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 β] [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 β] [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 β] [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) :

          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 β] [MonoidHomClass hom α β] {f : hom} :

          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 β] [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 β] [MonoidHomClass hom α β] {f : hom} (h : Continuous f) :
          theorem CauchySeq.add {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {ι : Type u_3} [SemilatticeSup ι] {u : ια} {v : ια} (hu : CauchySeq u) (hv : CauchySeq v) :
          CauchySeq (u + v)
          theorem CauchySeq.mul {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] {ι : Type u_3} [SemilatticeSup ι] {u : ια} {v : ια} (hu : CauchySeq u) (hv : CauchySeq v) :
          CauchySeq (u * v)
          theorem CauchySeq.add_const {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {ι : Type u_3} [SemilatticeSup ι] {u : ια} {x : α} (hu : CauchySeq u) :
          CauchySeq fun n => u n + x
          theorem CauchySeq.mul_const {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] {ι : Type u_3} [SemilatticeSup ι] {u : ια} {x : α} (hu : CauchySeq u) :
          CauchySeq fun n => u n * x
          theorem CauchySeq.const_add {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {ι : Type u_3} [SemilatticeSup ι] {u : ια} {x : α} (hu : CauchySeq u) :
          CauchySeq fun n => x + u n
          theorem CauchySeq.const_mul {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] {ι : Type u_3} [SemilatticeSup ι] {u : ια} {x : α} (hu : CauchySeq u) :
          CauchySeq fun n => x * u n
          theorem CauchySeq.neg {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {ι : Type u_3} [SemilatticeSup ι] {u : ια} (h : CauchySeq u) :
          theorem CauchySeq.inv {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] {ι : Type u_3} [SemilatticeSup ι] {u : ια} (h : CauchySeq u) :
          theorem totallyBounded_iff_subset_finite_iUnion_nhds_zero {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {s : Set α} :
          TotallyBounded s ∀ (U : Set α), U nhds 0t, Set.Finite t s ⋃ (y : α) (_ : y t), y +ᵥ U
          theorem totallyBounded_iff_subset_finite_iUnion_nhds_one {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] {s : Set α} :
          TotallyBounded s ∀ (U : Set α), U nhds 1t, Set.Finite t s ⋃ (y : α) (_ : y t), 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_3 (G : Type u_1) [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] :
          (Filter.lift' (Filter.comap (fun p => p.snd - p.fst) (nhds 0)) fun s => compRel s s) Filter.comap (fun p => p.snd - p.fst) (nhds 0)
          theorem TopologicalAddGroup.toUniformSpace.proof_4 (G : Type u_1) [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (S : Set G) :
          IsOpen S ∀ (a : G), a S{p | p.fst = ap.snd S} Filter.comap (fun p => p.snd - p.fst) (nhds 0)
          theorem TopologicalAddGroup.toUniformSpace.proof_2 (G : Type u_1) [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] :
          Filter.Tendsto Prod.swap (Filter.comap (fun p => p.snd - p.fst) (nhds 0)) (Filter.comap (fun p => p.snd - p.fst) (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
          • One or more equations did not get rendered due to their size.
          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
            • One or more equations did not get rendered due to their size.
            Instances For
              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 { x // x MonoidHom.range f }) :
              Filter.Tendsto (f) Filter.cofinite (Filter.cocompact G)
              abbrev TopologicalAddGroup.tendstoUniformly_iff.match_1 {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] :
              ∀ (x : Set (G × G)) (motive : x uniformity GProp) (x_1 : x uniformity G), (∀ (u : Set G) (hu : u nhds 0) (hv : (fun p => p.snd - p.fst) ⁻¹' u x), motive (_ : t, t nhds 0 (fun p => p.snd - p.fst) ⁻¹' t x)) → motive x_1
              Equations
              Instances For
                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 ∀ (u : Set G), u nhds 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 ∀ (u : Set G), u nhds 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 ∀ (u : Set G), u nhds 0∀ᶠ (i : ι) in p, ∀ (a : α), a sF 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 ∀ (u : Set G), u nhds 1∀ᶠ (i : ι) in p, ∀ (a : α), a sF i a / f a u
                abbrev TopologicalAddGroup.tendstoLocallyUniformly_iff.match_1 {G : Type u_3} [AddGroup G] {ι : Type u_2} {α : Type u_1} [TopologicalSpace α] (F : ιαG) (f : αG) (p : Filter ι) (x : α) (u : Set G) :
                ∀ (x : Set α) (motive : (x nhds x ∀ᶠ (i : ι) in p, ∀ (a : α), a xF i a - f a u) → Prop) (x_1 : x nhds x ∀ᶠ (i : ι) in p, ∀ (a : α), a xF i a - f a u), (∀ (h : x nhds x) (hp : ∀ᶠ (i : ι) in p, ∀ (a : α), a xF i a - f a u), motive (_ : x nhds x ∀ᶠ (i : ι) in p, ∀ (a : α), a xF i a - f a u)) → motive x_1
                Equations
                Instances For
                  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 ∀ (u : Set G), u nhds 0∀ (x : α), t, t nhds x ∀ᶠ (i : ι) in p, ∀ (a : α), a tF 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 ∀ (u : Set G), u nhds 1∀ (x : α), t, t nhds x ∀ᶠ (i : ι) in p, ∀ (a : α), a tF i a / f a u
                  abbrev TopologicalAddGroup.tendstoLocallyUniformlyOn_iff.match_1 {G : Type u_3} [AddGroup G] {ι : Type u_2} {α : Type u_1} [TopologicalSpace α] (F : ιαG) (f : αG) (p : Filter ι) (s : Set α) (x : α) (u : Set G) :
                  ∀ (x : Set α) (motive : (x nhdsWithin x s ∀ᶠ (i : ι) in p, ∀ (a : α), a xF i a - f a u) → Prop) (x_1 : x nhdsWithin x s ∀ᶠ (i : ι) in p, ∀ (a : α), a xF i a - f a u), (∀ (h : x nhdsWithin x s) (hp : ∀ᶠ (i : ι) in p, ∀ (a : α), a xF i a - f a u), motive (_ : x nhdsWithin x s ∀ᶠ (i : ι) in p, ∀ (a : α), a xF i a - f a u)) → motive x_1
                  Equations
                  Instances For
                    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 ∀ (u : Set G), u nhds 0∀ (x : α), x st, t nhdsWithin x s ∀ᶠ (i : ι) in p, ∀ (a : α), a tF 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 ∀ (u : Set G), u nhds 1∀ (x : α), x st, t nhdsWithin x s ∀ᶠ (i : ι) in p, ∀ (a : α), a tF 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 β] [AddMonoidHomClass hom β α] {e : hom} (de : DenseInducing e) (x₀ : α) :
                    Filter.Tendsto (fun t => t.snd - t.fst) (Filter.comap (fun p => (e p.fst, e p.snd)) (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 β] [MonoidHomClass hom β α] {e : hom} (de : DenseInducing e) (x₀ : α) :
                    Filter.Tendsto (fun t => t.snd / t.fst) (Filter.comap (fun p => (e p.fst, e p.snd)) (nhds (x₀, x₀))) (nhds 1)
                    theorem DenseInducing.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] [UniformAddGroup G] [SeparatedSpace G] [CompleteSpace G] {e : β →+ α} (de : DenseInducing e) {f : δ →+ γ} (df : DenseInducing f) {φ : β →+ δ →+ G} (hφ : Continuous fun p => ↑(φ p.fst) p.snd) :
                    Continuous (DenseInducing.extend (_ : DenseInducing fun p => (e p.fst, f p.snd)) fun p => ↑(φ p.fst) p.snd)

                    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

                    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