Documentation

Mathlib.Topology.Algebra.UniformGroup.Basic

Uniform structure on topological groups #

Main results #

theorem 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)
theorem 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)
theorem isUniformEmbedding_translate_mul {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] (a : α) :
IsUniformEmbedding fun (x : α) => x * a
theorem isUniformEmbedding_translate_add {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] (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.

theorem IsUniformInducing.uniformGroup {β : Type u_2} [Group β] {γ : Type u_3} [Group γ] [UniformSpace γ] [UniformGroup γ] [UniformSpace β] {F : Type u_4} [FunLike F β γ] [MonoidHomClass F β γ] (f : F) (hf : IsUniformInducing f) :
theorem IsUniformInducing.uniformAddGroup {β : Type u_2} [AddGroup β] {γ : Type u_3} [AddGroup γ] [UniformSpace γ] [UniformAddGroup γ] [UniformSpace β] {F : Type u_4} [FunLike F β γ] [AddMonoidHomClass F β γ] (f : F) (hf : IsUniformInducing f) :
@[deprecated IsUniformInducing.uniformGroup]
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 : IsUniformInducing f) :

Alias of IsUniformInducing.uniformGroup.

theorem UniformGroup.comap {β : Type u_2} [Group β] {γ : Type u_3} [Group γ] {u : UniformSpace γ} [UniformGroup γ] {F : Type u_4} [FunLike F β γ] [MonoidHomClass F β γ] (f : 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 Subgroup.uniformGroup {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] (S : Subgroup α) :
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 {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {ι : Type u_3} [Preorder ι] {u v : ια} (hu : CauchySeq u) (hv : CauchySeq v) :
CauchySeq (u + v)
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.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.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.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.inv {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] {ι : Type u_3} [Preorder ι] {u : ια} (h : CauchySeq u) :
theorem CauchySeq.neg {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {ι : Type u_3} [Preorder ι] {u : ια} (h : CauchySeq 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 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_inv {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] {s : Set α} (hs : TotallyBounded s) :
theorem totallyBounded_neg {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {s : Set α} (hs : TotallyBounded s) :
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.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.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 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 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.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.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 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 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.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.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 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 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.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.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 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 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 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 TopologicalGroup.tendstoUniformly_iff {ι : Type u_1} {α : Type u_2} {G : Type u_3} [Group G] [u : UniformSpace G] [TopologicalGroup G] (F : ιαG) (f : αG) (p : Filter ι) (hu : TopologicalGroup.toUniformSpace G = u) :
TendstoUniformly F f p u_1nhds 1, ∀ᶠ (i : ι) in p, ∀ (a : α), F i a / f a u_1
theorem TopologicalAddGroup.tendstoUniformly_iff {ι : Type u_1} {α : Type u_2} {G : Type u_3} [AddGroup G] [u : UniformSpace G] [TopologicalAddGroup G] (F : ιαG) (f : αG) (p : Filter ι) (hu : TopologicalAddGroup.toUniformSpace G = u) :
TendstoUniformly F f p u_1nhds 0, ∀ᶠ (i : ι) in p, ∀ (a : α), F i a - f a u_1
theorem TopologicalGroup.tendstoUniformlyOn_iff {ι : Type u_1} {α : Type u_2} {G : Type u_3} [Group G] [u : UniformSpace G] [TopologicalGroup G] (F : ιαG) (f : αG) (p : Filter ι) (s : Set α) (hu : TopologicalGroup.toUniformSpace G = u) :
TendstoUniformlyOn F f p s u_1nhds 1, ∀ᶠ (i : ι) in p, as, F i a / f a u_1
theorem TopologicalAddGroup.tendstoUniformlyOn_iff {ι : Type u_1} {α : Type u_2} {G : Type u_3} [AddGroup G] [u : UniformSpace G] [TopologicalAddGroup G] (F : ιαG) (f : αG) (p : Filter ι) (s : Set α) (hu : TopologicalAddGroup.toUniformSpace G = u) :
TendstoUniformlyOn F f p s u_1nhds 0, ∀ᶠ (i : ι) in p, as, F i a - f a u_1
theorem TopologicalGroup.tendstoLocallyUniformly_iff {ι : Type u_1} {α : Type u_2} {G : Type u_3} [Group G] [u : UniformSpace G] [TopologicalGroup G] [TopologicalSpace α] (F : ιαG) (f : αG) (p : Filter ι) (hu : TopologicalGroup.toUniformSpace G = u) :
TendstoLocallyUniformly F f p u_1nhds 1, ∀ (x : α), tnhds x, ∀ᶠ (i : ι) in p, at, F i a / f a u_1
theorem TopologicalAddGroup.tendstoLocallyUniformly_iff {ι : Type u_1} {α : Type u_2} {G : Type u_3} [AddGroup G] [u : UniformSpace G] [TopologicalAddGroup G] [TopologicalSpace α] (F : ιαG) (f : αG) (p : Filter ι) (hu : TopologicalAddGroup.toUniformSpace G = u) :
TendstoLocallyUniformly F f p u_1nhds 0, ∀ (x : α), tnhds x, ∀ᶠ (i : ι) in p, at, F i a - f a u_1
theorem TopologicalGroup.tendstoLocallyUniformlyOn_iff {ι : Type u_1} {α : Type u_2} {G : Type u_3} [Group G] [u : UniformSpace G] [TopologicalGroup G] [TopologicalSpace α] (F : ιαG) (f : αG) (p : Filter ι) (s : Set α) (hu : TopologicalGroup.toUniformSpace G = u) :
TendstoLocallyUniformlyOn F f p s u_1nhds 1, xs, tnhdsWithin x s, ∀ᶠ (i : ι) in p, at, F i a / f a u_1
theorem TopologicalAddGroup.tendstoLocallyUniformlyOn_iff {ι : Type u_1} {α : Type u_2} {G : Type u_3} [AddGroup G] [u : UniformSpace G] [TopologicalAddGroup G] [TopologicalSpace α] (F : ιαG) (f : αG) (p : Filter ι) (s : Set α) (hu : TopologicalAddGroup.toUniformSpace G = u) :
TendstoLocallyUniformlyOn F f p s u_1nhds 0, xs, tnhdsWithin x s, ∀ᶠ (i : ι) in p, at, F i a - f a u_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 group G by a normal subgroup is itself complete. N. Bourbaki, General Topology, IX.3.1 Proposition 4

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.

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

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.

theorem 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

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.

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

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.