mathlib documentation

topology.algebra.uniform_group

Uniform structure on topological groups #

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

Main declarations #

Main results #

@[class]
structure uniform_group (α : Type u_3) [uniform_space α] [group α] :
Prop

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

Instances of this typeclass
@[class]
structure uniform_add_group (α : Type u_3) [uniform_space α] [add_group α] :
Prop

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

Instances of this typeclass
theorem uniform_group.mk' {α : Type u_1} [uniform_space α] [group α] (h₁ : uniform_continuous (λ (p : α × α), p.fst * p.snd)) (h₂ : uniform_continuous (λ (p : α), p⁻¹)) :
theorem uniform_add_group.mk' {α : Type u_1} [uniform_space α] [add_group α] (h₁ : uniform_continuous (λ (p : α × α), p.fst + p.snd)) (h₂ : uniform_continuous (λ (p : α), -p)) :
theorem uniform_continuous_div {α : Type u_1} [uniform_space α] [group α] [uniform_group α] :
uniform_continuous (λ (p : α × α), p.fst / p.snd)
theorem uniform_continuous_sub {α : Type u_1} [uniform_space α] [add_group α] [uniform_add_group α] :
uniform_continuous (λ (p : α × α), p.fst - p.snd)
theorem uniform_continuous.sub {α : Type u_1} {β : Type u_2} [uniform_space α] [add_group α] [uniform_add_group α] [uniform_space β] {f g : β → α} (hf : uniform_continuous f) (hg : uniform_continuous g) :
uniform_continuous (λ (x : β), f x - g x)
theorem uniform_continuous.div {α : Type u_1} {β : Type u_2} [uniform_space α] [group α] [uniform_group α] [uniform_space β] {f g : β → α} (hf : uniform_continuous f) (hg : uniform_continuous g) :
uniform_continuous (λ (x : β), f x / g x)
theorem uniform_continuous.neg {α : Type u_1} {β : Type u_2} [uniform_space α] [add_group α] [uniform_add_group α] [uniform_space β] {f : β → α} (hf : uniform_continuous f) :
uniform_continuous (λ (x : β), -f x)
theorem uniform_continuous.inv {α : Type u_1} {β : Type u_2} [uniform_space α] [group α] [uniform_group α] [uniform_space β] {f : β → α} (hf : uniform_continuous f) :
uniform_continuous (λ (x : β), (f x)⁻¹)
theorem uniform_continuous_inv {α : Type u_1} [uniform_space α] [group α] [uniform_group α] :
uniform_continuous (λ (x : α), x⁻¹)
theorem uniform_continuous_neg {α : Type u_1} [uniform_space α] [add_group α] [uniform_add_group α] :
uniform_continuous (λ (x : α), -x)
theorem uniform_continuous.add {α : Type u_1} {β : Type u_2} [uniform_space α] [add_group α] [uniform_add_group α] [uniform_space β] {f g : β → α} (hf : uniform_continuous f) (hg : uniform_continuous g) :
uniform_continuous (λ (x : β), f x + g x)
theorem uniform_continuous.mul {α : Type u_1} {β : Type u_2} [uniform_space α] [group α] [uniform_group α] [uniform_space β] {f g : β → α} (hf : uniform_continuous f) (hg : uniform_continuous g) :
uniform_continuous (λ (x : β), f x * g x)
theorem uniform_continuous_mul {α : Type u_1} [uniform_space α] [group α] [uniform_group α] :
uniform_continuous (λ (p : α × α), p.fst * p.snd)
theorem uniform_continuous_add {α : Type u_1} [uniform_space α] [add_group α] [uniform_add_group α] :
uniform_continuous (λ (p : α × α), p.fst + p.snd)
theorem uniform_continuous.const_nsmul {α : Type u_1} {β : Type u_2} [uniform_space α] [add_group α] [uniform_add_group α] [uniform_space β] {f : β → α} (hf : uniform_continuous f) (n : ) :
uniform_continuous (λ (x : β), n f x)
theorem uniform_continuous.pow_const {α : Type u_1} {β : Type u_2} [uniform_space α] [group α] [uniform_group α] [uniform_space β] {f : β → α} (hf : uniform_continuous f) (n : ) :
uniform_continuous (λ (x : β), f x ^ n)
theorem uniform_continuous_pow_const {α : Type u_1} [uniform_space α] [group α] [uniform_group α] (n : ) :
uniform_continuous (λ (x : α), x ^ n)
theorem uniform_continuous_const_nsmul {α : Type u_1} [uniform_space α] [add_group α] [uniform_add_group α] (n : ) :
uniform_continuous (λ (x : α), n x)
theorem uniform_continuous.zpow_const {α : Type u_1} {β : Type u_2} [uniform_space α] [group α] [uniform_group α] [uniform_space β] {f : β → α} (hf : uniform_continuous f) (n : ) :
uniform_continuous (λ (x : β), f x ^ n)
theorem uniform_continuous.const_zsmul {α : Type u_1} {β : Type u_2} [uniform_space α] [add_group α] [uniform_add_group α] [uniform_space β] {f : β → α} (hf : uniform_continuous f) (n : ) :
uniform_continuous (λ (x : β), n f x)
theorem uniform_continuous_zpow_const {α : Type u_1} [uniform_space α] [group α] [uniform_group α] (n : ) :
uniform_continuous (λ (x : α), x ^ n)
theorem uniform_continuous_const_zsmul {α : Type u_1} [uniform_space α] [add_group α] [uniform_add_group α] (n : ) :
uniform_continuous (λ (x : α), n x)
@[protected, instance]
@[protected, instance]
def prod.uniform_add_group {α : Type u_1} {β : Type u_2} [uniform_space α] [add_group α] [uniform_add_group α] [uniform_space β] [add_group β] [uniform_add_group β] :
@[protected, instance]
def prod.uniform_group {α : Type u_1} {β : Type u_2} [uniform_space α] [group α] [uniform_group α] [uniform_space β] [group β] [uniform_group β] :
theorem uniformity_translate_add {α : Type u_1} [uniform_space α] [add_group α] [uniform_add_group α] (a : α) :
filter.map (λ (x : α × α), (x.fst + a, x.snd + a)) (uniformity α) = uniformity α
theorem uniformity_translate_mul {α : Type u_1} [uniform_space α] [group α] [uniform_group α] (a : α) :
filter.map (λ (x : α × α), (x.fst * a, x.snd * a)) (uniformity α) = uniformity α
theorem uniform_embedding_translate_mul {α : Type u_1} [uniform_space α] [group α] [uniform_group α] (a : α) :
uniform_embedding (λ (x : α), x * a)
theorem uniform_embedding_translate_add {α : Type u_1} [uniform_space α] [add_group α] [uniform_add_group α] (a : α) :
uniform_embedding (λ (x : α), x + a)
@[protected, instance]
@[protected, instance]
@[protected, instance]
def subgroup.uniform_group {α : Type u_1} [uniform_space α] [group α] [uniform_group α] (S : subgroup α) :
@[protected, instance]
theorem uniform_add_group_Inf {β : Type u_2} [add_group β] {us : set (uniform_space β)} (h : ∀ (u : uniform_space β), u usuniform_add_group β) :
theorem uniform_group_Inf {β : Type u_2} [group β] {us : set (uniform_space β)} (h : ∀ (u : uniform_space β), u usuniform_group β) :
theorem uniform_group_infi {β : Type u_2} [group β] {ι : Sort u_1} {us' : ι → uniform_space β} (h' : ∀ (i : ι), uniform_group β) :
theorem uniform_add_group_infi {β : Type u_2} [add_group β] {ι : Sort u_1} {us' : ι → uniform_space β} (h' : ∀ (i : ι), uniform_add_group β) :
theorem uniform_group_inf {β : Type u_2} [group β] {u₁ u₂ : uniform_space β} (h₁ : uniform_group β) (h₂ : uniform_group β) :
theorem uniform_add_group_inf {β : Type u_2} [add_group β] {u₁ u₂ : uniform_space β} (h₁ : uniform_add_group β) (h₂ : uniform_add_group β) :
theorem uniform_add_group_comap {β : Type u_2} [add_group β] {γ : Type u_1} [add_group γ] {u : uniform_space γ} [uniform_add_group γ] {F : Type u_3} [add_monoid_hom_class F β γ] (f : F) :
theorem uniform_group_comap {β : Type u_2} [group β] {γ : Type u_1} [group γ] {u : uniform_space γ} [uniform_group γ] {F : Type u_3} [monoid_hom_class F β γ] (f : F) :
theorem uniformity_eq_comap_nhds_one (α : Type u_1) [uniform_space α] [group α] [uniform_group α] :
uniformity α = filter.comap (λ (x : α × α), x.snd / x.fst) (nhds 1)
theorem uniformity_eq_comap_nhds_zero (α : Type u_1) [uniform_space α] [add_group α] [uniform_add_group α] :
uniformity α = filter.comap (λ (x : α × α), x.snd - x.fst) (nhds 0)
theorem uniformity_eq_comap_nhds_one_swapped (α : Type u_1) [uniform_space α] [group α] [uniform_group α] :
uniformity α = filter.comap (λ (x : α × α), x.fst / x.snd) (nhds 1)
theorem uniformity_eq_comap_nhds_zero_swapped (α : Type u_1) [uniform_space α] [add_group α] [uniform_add_group α] :
uniformity α = filter.comap (λ (x : α × α), x.fst - x.snd) (nhds 0)
theorem uniformity_eq_comap_inv_mul_nhds_one {α : Type u_1} [uniform_space α] [group α] [uniform_group α] :
uniformity α = filter.comap (λ (x : α × α), (x.fst)⁻¹ * x.snd) (nhds 1)
theorem uniformity_eq_comap_neg_add_nhds_zero {α : Type u_1} [uniform_space α] [add_group α] [uniform_add_group α] :
uniformity α = filter.comap (λ (x : α × α), -x.fst + x.snd) (nhds 0)
theorem uniformity_eq_comap_neg_add_nhds_zero_swapped {α : Type u_1} [uniform_space α] [add_group α] [uniform_add_group α] :
uniformity α = filter.comap (λ (x : α × α), -x.snd + x.fst) (nhds 0)
theorem uniformity_eq_comap_inv_mul_nhds_one_swapped {α : Type u_1} [uniform_space α] [group α] [uniform_group α] :
uniformity α = filter.comap (λ (x : α × α), (x.snd)⁻¹ * x.fst) (nhds 1)
theorem filter.has_basis.uniformity_of_nhds_one {α : Type u_1} [uniform_space α] [group α] [uniform_group α] {ι : Sort u_2} {p : ι → Prop} {U : ι → set α} (h : (nhds 1).has_basis p U) :
(uniformity α).has_basis p (λ (i : ι), {x : α × α | x.snd / x.fst U i})
theorem filter.has_basis.uniformity_of_nhds_zero {α : Type u_1} [uniform_space α] [add_group α] [uniform_add_group α] {ι : Sort u_2} {p : ι → Prop} {U : ι → set α} (h : (nhds 0).has_basis p U) :
(uniformity α).has_basis p (λ (i : ι), {x : α × α | x.snd - x.fst U i})
theorem filter.has_basis.uniformity_of_nhds_zero_neg_add {α : Type u_1} [uniform_space α] [add_group α] [uniform_add_group α] {ι : Sort u_2} {p : ι → Prop} {U : ι → set α} (h : (nhds 0).has_basis p U) :
(uniformity α).has_basis p (λ (i : ι), {x : α × α | -x.fst + x.snd U i})
theorem filter.has_basis.uniformity_of_nhds_one_inv_mul {α : Type u_1} [uniform_space α] [group α] [uniform_group α] {ι : Sort u_2} {p : ι → Prop} {U : ι → set α} (h : (nhds 1).has_basis p U) :
(uniformity α).has_basis p (λ (i : ι), {x : α × α | (x.fst)⁻¹ * x.snd U i})
theorem filter.has_basis.uniformity_of_nhds_zero_swapped {α : Type u_1} [uniform_space α] [add_group α] [uniform_add_group α] {ι : Sort u_2} {p : ι → Prop} {U : ι → set α} (h : (nhds 0).has_basis p U) :
(uniformity α).has_basis p (λ (i : ι), {x : α × α | x.fst - x.snd U i})
theorem filter.has_basis.uniformity_of_nhds_one_swapped {α : Type u_1} [uniform_space α] [group α] [uniform_group α] {ι : Sort u_2} {p : ι → Prop} {U : ι → set α} (h : (nhds 1).has_basis p U) :
(uniformity α).has_basis p (λ (i : ι), {x : α × α | x.fst / x.snd U i})
theorem filter.has_basis.uniformity_of_nhds_one_inv_mul_swapped {α : Type u_1} [uniform_space α] [group α] [uniform_group α] {ι : Sort u_2} {p : ι → Prop} {U : ι → set α} (h : (nhds 1).has_basis p U) :
(uniformity α).has_basis p (λ (i : ι), {x : α × α | (x.snd)⁻¹ * x.fst U i})
theorem filter.has_basis.uniformity_of_nhds_zero_neg_add_swapped {α : Type u_1} [uniform_space α] [add_group α] [uniform_add_group α] {ι : Sort u_2} {p : ι → Prop} {U : ι → set α} (h : (nhds 0).has_basis p U) :
(uniformity α).has_basis p (λ (i : ι), {x : α × α | -x.snd + x.fst U i})
theorem add_group_separation_rel {α : Type u_1} [uniform_space α] [add_group α] [uniform_add_group α] (x y : α) :
(x, y) separation_rel α x - y closure {0}
theorem group_separation_rel {α : Type u_1} [uniform_space α] [group α] [uniform_group α] (x y : α) :
(x, y) separation_rel α x / y closure {1}
theorem uniform_continuous_of_tendsto_one {α : Type u_1} {β : Type u_2} [uniform_space α] [group α] [uniform_group α] {hom : Type u_3} [uniform_space β] [group β] [uniform_group β] [monoid_hom_class hom α β] {f : hom} (h : filter.tendsto f (nhds 1) (nhds 1)) :
theorem uniform_continuous_of_tendsto_zero {α : Type u_1} {β : Type u_2} [uniform_space α] [add_group α] [uniform_add_group α] {hom : Type u_3} [uniform_space β] [add_group β] [uniform_add_group β] [add_monoid_hom_class hom α β] {f : hom} (h : filter.tendsto f (nhds 0) (nhds 0)) :
theorem uniform_continuous_of_continuous_at_one {α : Type u_1} {β : Type u_2} [uniform_space α] [group α] [uniform_group α] {hom : Type u_3} [uniform_space β] [group β] [uniform_group β] [monoid_hom_class hom α β] (f : hom) (hf : continuous_at f 1) :

A group homomorphism (a bundled morphism of a type that implements monoid_hom_class) between two uniform groups is uniformly continuous provided that it is continuous at one. See also continuous_of_continuous_at_one.

theorem uniform_continuous_of_continuous_at_zero {α : Type u_1} {β : Type u_2} [uniform_space α] [add_group α] [uniform_add_group α] {hom : Type u_3} [uniform_space β] [add_group β] [uniform_add_group β] [add_monoid_hom_class hom α β] (f : hom) (hf : continuous_at f 0) :

An additive group homomorphism (a bundled morphism of a type that implements add_monoid_hom_class) between two uniform additive groups is uniformly continuous provided that it is continuous at zero. See also continuous_of_continuous_at_zero.

theorem monoid_hom.uniform_continuous_of_continuous_at_one {α : Type u_1} {β : Type u_2} [uniform_space α] [group α] [uniform_group α] [uniform_space β] [group β] [uniform_group β] (f : α →* β) (hf : continuous_at f 1) :
theorem uniform_group.uniform_continuous_iff_open_ker {α : Type u_1} {β : Type u_2} [uniform_space α] [group α] [uniform_group α] {hom : Type u_3} [uniform_space β] [discrete_topology β] [group β] [uniform_group β] [monoid_hom_class 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 uniform_add_group.uniform_continuous_iff_open_ker {α : Type u_1} {β : Type u_2} [uniform_space α] [add_group α] [uniform_add_group α] {hom : Type u_3} [uniform_space β] [discrete_topology β] [add_group β] [uniform_add_group β] [add_monoid_hom_class hom α β] {f : hom} :

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

theorem uniform_continuous_monoid_hom_of_continuous {α : Type u_1} {β : Type u_2} [uniform_space α] [group α] [uniform_group α] {hom : Type u_3} [uniform_space β] [group β] [uniform_group β] [monoid_hom_class hom α β] {f : hom} (h : continuous f) :
theorem uniform_continuous_add_monoid_hom_of_continuous {α : Type u_1} {β : Type u_2} [uniform_space α] [add_group α] [uniform_add_group α] {hom : Type u_3} [uniform_space β] [add_group β] [uniform_add_group β] [add_monoid_hom_class hom α β] {f : hom} (h : continuous f) :
theorem cauchy_seq.add {α : Type u_1} [uniform_space α] [add_group α] [uniform_add_group α] {ι : Type u_2} [semilattice_sup ι] {u v : ι → α} (hu : cauchy_seq u) (hv : cauchy_seq v) :
theorem cauchy_seq.mul {α : Type u_1} [uniform_space α] [group α] [uniform_group α] {ι : Type u_2} [semilattice_sup ι] {u v : ι → α} (hu : cauchy_seq u) (hv : cauchy_seq v) :
theorem cauchy_seq.mul_const {α : Type u_1} [uniform_space α] [group α] [uniform_group α] {ι : Type u_2} [semilattice_sup ι] {u : ι → α} {x : α} (hu : cauchy_seq u) :
cauchy_seq (λ (n : ι), u n * x)
theorem cauchy_seq.add_const {α : Type u_1} [uniform_space α] [add_group α] [uniform_add_group α] {ι : Type u_2} [semilattice_sup ι] {u : ι → α} {x : α} (hu : cauchy_seq u) :
cauchy_seq (λ (n : ι), u n + x)
theorem cauchy_seq.const_mul {α : Type u_1} [uniform_space α] [group α] [uniform_group α] {ι : Type u_2} [semilattice_sup ι] {u : ι → α} {x : α} (hu : cauchy_seq u) :
cauchy_seq (λ (n : ι), x * u n)
theorem cauchy_seq.const_add {α : Type u_1} [uniform_space α] [add_group α] [uniform_add_group α] {ι : Type u_2} [semilattice_sup ι] {u : ι → α} {x : α} (hu : cauchy_seq u) :
cauchy_seq (λ (n : ι), x + u n)
theorem cauchy_seq.inv {α : Type u_1} [uniform_space α] [group α] [uniform_group α] {ι : Type u_2} [semilattice_sup ι] {u : ι → α} (h : cauchy_seq u) :
theorem cauchy_seq.neg {α : Type u_1} [uniform_space α] [add_group α] [uniform_add_group α] {ι : Type u_2} [semilattice_sup ι] {u : ι → α} (h : cauchy_seq u) :
theorem totally_bounded_iff_subset_finite_Union_nhds_zero {α : Type u_1} [uniform_space α] [add_group α] [uniform_add_group α] {s : set α} :
totally_bounded s ∀ (U : set α), U nhds 0(∃ (t : set α), t.finite s ⋃ (y : α) (H : y t), y +ᵥ U)
theorem totally_bounded_iff_subset_finite_Union_nhds_one {α : Type u_1} [uniform_space α] [group α] [uniform_group α] {s : set α} :
totally_bounded s ∀ (U : set α), U nhds 1(∃ (t : set α), t.finite s ⋃ (y : α) (H : y t), y U)
theorem tendsto_uniformly_on_filter.mul {α : Type u_1} {β : Type u_2} [uniform_space α] [group α] [uniform_group α] {ι : Type u_3} {l : filter ι} {l' : filter β} {f f' : ι → β → α} {g g' : β → α} (hf : tendsto_uniformly_on_filter f g l l') (hf' : tendsto_uniformly_on_filter f' g' l l') :
tendsto_uniformly_on_filter (f * f') (g * g') l l'
theorem tendsto_uniformly_on_filter.add {α : Type u_1} {β : Type u_2} [uniform_space α] [add_group α] [uniform_add_group α] {ι : Type u_3} {l : filter ι} {l' : filter β} {f f' : ι → β → α} {g g' : β → α} (hf : tendsto_uniformly_on_filter f g l l') (hf' : tendsto_uniformly_on_filter f' g' l l') :
tendsto_uniformly_on_filter (f + f') (g + g') l l'
theorem tendsto_uniformly_on_filter.sub {α : Type u_1} {β : Type u_2} [uniform_space α] [add_group α] [uniform_add_group α] {ι : Type u_3} {l : filter ι} {l' : filter β} {f f' : ι → β → α} {g g' : β → α} (hf : tendsto_uniformly_on_filter f g l l') (hf' : tendsto_uniformly_on_filter f' g' l l') :
tendsto_uniformly_on_filter (f - f') (g - g') l l'
theorem tendsto_uniformly_on_filter.div {α : Type u_1} {β : Type u_2} [uniform_space α] [group α] [uniform_group α] {ι : Type u_3} {l : filter ι} {l' : filter β} {f f' : ι → β → α} {g g' : β → α} (hf : tendsto_uniformly_on_filter f g l l') (hf' : tendsto_uniformly_on_filter f' g' l l') :
tendsto_uniformly_on_filter (f / f') (g / g') l l'
theorem tendsto_uniformly_on.mul {α : Type u_1} {β : Type u_2} [uniform_space α] [group α] [uniform_group α] {ι : Type u_3} {l : filter ι} {f f' : ι → β → α} {g g' : β → α} {s : set β} (hf : tendsto_uniformly_on f g l s) (hf' : tendsto_uniformly_on f' g' l s) :
tendsto_uniformly_on (f * f') (g * g') l s
theorem tendsto_uniformly_on.add {α : Type u_1} {β : Type u_2} [uniform_space α] [add_group α] [uniform_add_group α] {ι : Type u_3} {l : filter ι} {f f' : ι → β → α} {g g' : β → α} {s : set β} (hf : tendsto_uniformly_on f g l s) (hf' : tendsto_uniformly_on f' g' l s) :
tendsto_uniformly_on (f + f') (g + g') l s
theorem tendsto_uniformly_on.div {α : Type u_1} {β : Type u_2} [uniform_space α] [group α] [uniform_group α] {ι : Type u_3} {l : filter ι} {f f' : ι → β → α} {g g' : β → α} {s : set β} (hf : tendsto_uniformly_on f g l s) (hf' : tendsto_uniformly_on f' g' l s) :
tendsto_uniformly_on (f / f') (g / g') l s
theorem tendsto_uniformly_on.sub {α : Type u_1} {β : Type u_2} [uniform_space α] [add_group α] [uniform_add_group α] {ι : Type u_3} {l : filter ι} {f f' : ι → β → α} {g g' : β → α} {s : set β} (hf : tendsto_uniformly_on f g l s) (hf' : tendsto_uniformly_on f' g' l s) :
tendsto_uniformly_on (f - f') (g - g') l s
theorem tendsto_uniformly.add {α : Type u_1} {β : Type u_2} [uniform_space α] [add_group α] [uniform_add_group α] {ι : Type u_3} {l : filter ι} {f f' : ι → β → α} {g g' : β → α} (hf : tendsto_uniformly f g l) (hf' : tendsto_uniformly f' g' l) :
tendsto_uniformly (f + f') (g + g') l
theorem tendsto_uniformly.mul {α : Type u_1} {β : Type u_2} [uniform_space α] [group α] [uniform_group α] {ι : Type u_3} {l : filter ι} {f f' : ι → β → α} {g g' : β → α} (hf : tendsto_uniformly f g l) (hf' : tendsto_uniformly f' g' l) :
tendsto_uniformly (f * f') (g * g') l
theorem tendsto_uniformly.div {α : Type u_1} {β : Type u_2} [uniform_space α] [group α] [uniform_group α] {ι : Type u_3} {l : filter ι} {f f' : ι → β → α} {g g' : β → α} (hf : tendsto_uniformly f g l) (hf' : tendsto_uniformly f' g' l) :
tendsto_uniformly (f / f') (g / g') l
theorem tendsto_uniformly.sub {α : Type u_1} {β : Type u_2} [uniform_space α] [add_group α] [uniform_add_group α] {ι : Type u_3} {l : filter ι} {f f' : ι → β → α} {g g' : β → α} (hf : tendsto_uniformly f g l) (hf' : tendsto_uniformly f' g' l) :
tendsto_uniformly (f - f') (g - g') l
theorem uniform_cauchy_seq_on.add {α : Type u_1} {β : Type u_2} [uniform_space α] [add_group α] [uniform_add_group α] {ι : Type u_3} {l : filter ι} {f f' : ι → β → α} {s : set β} (hf : uniform_cauchy_seq_on f l s) (hf' : uniform_cauchy_seq_on f' l s) :
theorem uniform_cauchy_seq_on.mul {α : Type u_1} {β : Type u_2} [uniform_space α] [group α] [uniform_group α] {ι : Type u_3} {l : filter ι} {f f' : ι → β → α} {s : set β} (hf : uniform_cauchy_seq_on f l s) (hf' : uniform_cauchy_seq_on f' l s) :
theorem uniform_cauchy_seq_on.sub {α : Type u_1} {β : Type u_2} [uniform_space α] [add_group α] [uniform_add_group α] {ι : Type u_3} {l : filter ι} {f f' : ι → β → α} {s : set β} (hf : uniform_cauchy_seq_on f l s) (hf' : uniform_cauchy_seq_on f' l s) :
theorem uniform_cauchy_seq_on.div {α : Type u_1} {β : Type u_2} [uniform_space α] [group α] [uniform_group α] {ι : Type u_3} {l : filter ι} {f f' : ι → β → α} {s : set β} (hf : uniform_cauchy_seq_on f l s) (hf' : uniform_cauchy_seq_on f' l s) :

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 uniform_add_group structure. Two important special cases where they do coincide are for commutative additive groups (see topological_add_comm_group_is_uniform) and for compact additive groups (see topological_add_comm_group_is_uniform_of_compact_space).

Equations

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 uniform_group structure. Two important special cases where they do coincide are for commutative groups (see topological_comm_group_is_uniform) and for compact groups (see topological_group_is_uniform_of_compact_space).

Equations
theorem uniformity_eq_comap_nhds_one' (G : Type u_1) [group G] [topological_space G] [topological_group G] :
uniformity G = filter.comap (λ (p : G × G), p.snd / p.fst) (nhds 1)
@[protected, instance]
theorem topological_group.tendsto_uniformly_iff {G : Type u_1} [group G] [topological_space G] [topological_group G] {ι : Type u_2} {α : Type u_3} (F : ι → α → G) (f : α → G) (p : filter ι) :
tendsto_uniformly F f p ∀ (u : set G), u nhds 1(∀ᶠ (i : ι) in p, ∀ (a : α), F i a / f a u)
theorem topological_add_group.tendsto_uniformly_iff {G : Type u_1} [add_group G] [topological_space G] [topological_add_group G] {ι : Type u_2} {α : Type u_3} (F : ι → α → G) (f : α → G) (p : filter ι) :
tendsto_uniformly F f p ∀ (u : set G), u nhds 0(∀ᶠ (i : ι) in p, ∀ (a : α), F i a - f a u)
theorem topological_add_group.tendsto_uniformly_on_iff {G : Type u_1} [add_group G] [topological_space G] [topological_add_group G] {ι : Type u_2} {α : Type u_3} (F : ι → α → G) (f : α → G) (p : filter ι) (s : set α) :
tendsto_uniformly_on F f p s ∀ (u : set G), u nhds 0(∀ᶠ (i : ι) in p, ∀ (a : α), a sF i a - f a u)
theorem topological_group.tendsto_uniformly_on_iff {G : Type u_1} [group G] [topological_space G] [topological_group G] {ι : Type u_2} {α : Type u_3} (F : ι → α → G) (f : α → G) (p : filter ι) (s : set α) :
tendsto_uniformly_on F f p s ∀ (u : set G), u nhds 1(∀ᶠ (i : ι) in p, ∀ (a : α), a sF i a / f a u)
theorem topological_add_group.tendsto_locally_uniformly_iff {G : Type u_1} [add_group G] [topological_space G] [topological_add_group G] {ι : Type u_2} {α : Type u_3} [topological_space α] (F : ι → α → G) (f : α → G) (p : filter ι) :
tendsto_locally_uniformly F f p ∀ (u : set G), u nhds 0∀ (x : α), ∃ (t : set α) (H : t nhds x), ∀ᶠ (i : ι) in p, ∀ (a : α), a tF i a - f a u
theorem topological_group.tendsto_locally_uniformly_iff {G : Type u_1} [group G] [topological_space G] [topological_group G] {ι : Type u_2} {α : Type u_3} [topological_space α] (F : ι → α → G) (f : α → G) (p : filter ι) :
tendsto_locally_uniformly F f p ∀ (u : set G), u nhds 1∀ (x : α), ∃ (t : set α) (H : t nhds x), ∀ᶠ (i : ι) in p, ∀ (a : α), a tF i a / f a u
theorem topological_group.tendsto_locally_uniformly_on_iff {G : Type u_1} [group G] [topological_space G] [topological_group G] {ι : Type u_2} {α : Type u_3} [topological_space α] (F : ι → α → G) (f : α → G) (p : filter ι) (s : set α) :
tendsto_locally_uniformly_on F f p s ∀ (u : set G), u nhds 1∀ (x : α), x s(∃ (t : set α) (H : t nhds_within x s), ∀ᶠ (i : ι) in p, ∀ (a : α), a tF i a / f a u)
theorem topological_add_group.tendsto_locally_uniformly_on_iff {G : Type u_1} [add_group G] [topological_space G] [topological_add_group G] {ι : Type u_2} {α : Type u_3} [topological_space α] (F : ι → α → G) (f : α → G) (p : filter ι) (s : set α) :
tendsto_locally_uniformly_on F f p s ∀ (u : set G), u nhds 0∀ (x : α), x s(∃ (t : set α) (H : t nhds_within x s), ∀ᶠ (i : ι) in p, ∀ (a : α), a tF i a - f a u)
theorem topological_add_group.t2_space_of_zero_sep {G : Type u_1} [add_comm_group G] [topological_space G] [topological_add_group G] (H : ∀ (x : G), x 0(∃ (U : set G) (H : U nhds 0), x U)) :
theorem topological_group.t2_space_of_one_sep {G : Type u_1} [comm_group G] [topological_space G] [topological_group G] (H : ∀ (x : G), x 1(∃ (U : set G) (H : U nhds 1), x U)) :
theorem tendsto_div_comap_self {α : Type u_1} {β : Type u_2} {hom : Type u_3} [topological_space α] [group α] [topological_group α] [topological_space β] [group β] [monoid_hom_class hom β α] {e : hom} (de : dense_inducing e) (x₀ : α) :
filter.tendsto (λ (t : β × β), t.snd / t.fst) (filter.comap (λ (p : β × β), (e p.fst, e p.snd)) (nhds (x₀, x₀))) (nhds 1)
theorem tendsto_sub_comap_self {α : Type u_1} {β : Type u_2} {hom : Type u_3} [topological_space α] [add_group α] [topological_add_group α] [topological_space β] [add_group β] [add_monoid_hom_class hom β α] {e : hom} (de : dense_inducing e) (x₀ : α) :
filter.tendsto (λ (t : β × β), t.snd - t.fst) (filter.comap (λ (p : β × β), (e p.fst, e p.snd)) (nhds (x₀, x₀))) (nhds 0)
theorem dense_inducing.extend_Z_bilin {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {G : Type u_5} [topological_space α] [add_comm_group α] [topological_add_group α] [topological_space β] [add_comm_group β] [topological_add_group β] [topological_space γ] [add_comm_group γ] [topological_add_group γ] [topological_space δ] [add_comm_group δ] [topological_add_group δ] [uniform_space G] [add_comm_group G] [uniform_add_group G] [separated_space G] [complete_space G] {e : β →+ α} (de : dense_inducing e) {f : δ →+ γ} (df : dense_inducing f) {φ : β →+ δ →+ G} (hφ : continuous (λ (p : β × δ), (φ p.fst) p.snd)) :
continuous (_.extend (λ (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.

@[protected, instance]

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 uniform_space instance by default, we must explicitly provide it in order to consider completeness. See quotient_group.complete_space for a version in which G is already equipped with a uniform structure.

@[protected, instance]

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 uniform_space instance by default, we must explicitly provide it in order to consider completeness. See quotient_add_group.complete_space for a version in which G is already equipped with a uniform structure.

@[protected, instance]

The quotient G ⧸ N of a complete first countable uniform group G by a normal subgroup is itself complete. In constrast to quotient_group.complete_space', 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 topological_group.to_uniform_space. In the most common use cases, this coincides (definitionally) with the uniform structure on the quotient obtained via other means.

@[protected, instance]

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 constrast to quotient_add_group.complete_space', 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 topological_add_group.to_uniform_space. 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.