Uniform structure on topological groups #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 #
uniform_groupanduniform_add_group: Multiplicative and additive uniform groups, that i.e., groups with uniformly continuous(*)and(⁻¹)/(+)and(-).
Main results #
-
topological_add_group.to_uniform_spaceandtopological_add_comm_group_is_uniformcan be used to construct a canonical uniformity for a topological add group. -
extension of ℤ-bilinear maps to complete groups (useful for ring completions)
-
quotient_group.complete_spaceandquotient_add_group.complete_spaceguarantee that quotients of first countable topological groups by normal subgroups are themselves complete. In particular, the quotient of a Banach space by a subspace is complete.
@[class]
- uniform_continuous_div : uniform_continuous (λ (p : α × α), p.fst / p.snd)
A uniform group is a group in which multiplication and inversion are uniformly continuous.
@[class]
- uniform_continuous_sub : uniform_continuous (λ (p : α × α), p.fst - p.snd)
A uniform additive group is an additive group in which addition and negation are uniformly continuous.
Instances of this typeclass
- seminormed_add_comm_group.to_uniform_add_group
- prod.uniform_add_group
- add_opposite.uniform_add_group
- add_subgroup.uniform_add_group
- real.uniform_add_group
- rat.uniform_add_group
- uniform_space.completion.uniform_add_group
- uniform_fun.uniform_add_group
- uniform_on_fun.uniform_add_group
- continuous_linear_map.uniform_add_group
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]
def
uniform_add_group.to_topological_add_group
{α : Type u_1}
[uniform_space α]
[add_group α]
[uniform_add_group α] :
@[protected, instance]
def
uniform_group.to_topological_group
{α : Type u_1}
[uniform_space α]
[group α]
[uniform_group α] :
@[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 β] :
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 β] :
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]
def
add_opposite.uniform_add_group
{α : Type u_1}
[uniform_space α]
[add_group α]
[uniform_add_group α] :
@[protected, instance]
def
subgroup.uniform_group
{α : Type u_1}
[uniform_space α]
[group α]
[uniform_group α]
(S : subgroup α) :
@[protected, instance]
def
add_subgroup.uniform_add_group
{α : Type u_1}
[uniform_space α]
[add_group α]
[uniform_add_group α]
(S : add_subgroup α) :
theorem
uniform_add_group_Inf
{β : Type u_2}
[add_group β]
{us : set (uniform_space β)}
(h : ∀ (u : uniform_space β), u ∈ us → uniform_add_group β) :
theorem
uniform_group_Inf
{β : Type u_2}
[group β]
{us : set (uniform_space β)}
(h : ∀ (u : uniform_space β), u ∈ us → uniform_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
uniform_add_group.ext
{G : Type u_1}
[add_group G]
{u v : uniform_space G}
(hu : uniform_add_group G)
(hv : uniform_add_group G)
(h : nhds 0 = nhds 0) :
u = v
theorem
uniform_group.ext
{G : Type u_1}
[group G]
{u v : uniform_space G}
(hu : uniform_group G)
(hv : uniform_group G)
(h : nhds 1 = nhds 1) :
u = v
theorem
uniform_group.ext_iff
{G : Type u_1}
[group G]
{u v : uniform_space G}
(hu : uniform_group G)
(hv : uniform_group G) :
theorem
uniform_add_group.ext_iff
{G : Type u_1}
[add_group G]
{u v : uniform_space G}
(hu : uniform_add_group G)
(hv : uniform_add_group G) :
theorem
uniform_add_group.uniformity_countably_generated
{α : Type u_1}
[uniform_space α]
[add_group α]
[uniform_add_group α]
[(nhds 0).is_countably_generated] :
theorem
uniform_group.uniformity_countably_generated
{α : Type u_1}
[uniform_space α]
[group α]
[uniform_group α]
[(nhds 1).is_countably_generated] :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
theorem
add_group_separation_rel
{α : Type u_1}
[uniform_space α]
[add_group α]
[uniform_add_group α]
(x y : α) :
theorem
group_separation_rel
{α : Type u_1}
[uniform_space α]
[group α]
[uniform_group α]
(x y : α) :
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
add_monoid_hom.uniform_continuous_of_continuous_at_zero
{α : Type u_1}
{β : Type u_2}
[uniform_space α]
[add_group α]
[uniform_add_group α]
[uniform_space β]
[add_group β]
[uniform_add_group β]
(f : α →+ β)
(hf : continuous_at ⇑f 0) :
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) :
cauchy_seq (u + 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) :
cauchy_seq (u * 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) :
cauchy_seq (-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) :
uniform_cauchy_seq_on (f + 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) :
uniform_cauchy_seq_on (f * 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) :
uniform_cauchy_seq_on (f - 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) :
uniform_cauchy_seq_on (f / f') l s
def
topological_add_group.to_uniform_space
(G : Type u_1)
[add_group G]
[topological_space G]
[topological_add_group G] :
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
- topological_add_group.to_uniform_space G = {to_topological_space := _inst_2, to_core := {uniformity := filter.comap (λ (p : G × G), p.snd - p.fst) (nhds 0), refl := _, symm := _, comp := _}, is_open_uniformity := _}
def
topological_group.to_uniform_space
(G : Type u_1)
[group G]
[topological_space G]
[topological_group G] :
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
- topological_group.to_uniform_space G = {to_topological_space := _inst_2, to_core := {uniformity := filter.comap (λ (p : G × G), p.snd / p.fst) (nhds 1), refl := _, symm := _, comp := _}, is_open_uniformity := _}
theorem
uniformity_eq_comap_nhds_zero'
(G : Type u_1)
[add_group G]
[topological_space G]
[topological_add_group G] :
uniformity G = filter.comap (λ (p : G × G), p.snd - p.fst) (nhds 0)
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)
theorem
topological_add_group_is_uniform_of_compact_space
(G : Type u_1)
[add_group G]
[topological_space G]
[topological_add_group G]
[compact_space G] :
theorem
topological_group_is_uniform_of_compact_space
(G : Type u_1)
[group G]
[topological_space G]
[topological_group G]
[compact_space G] :
@[protected, instance]
def
add_subgroup.is_closed_of_discrete
{G : Type u_1}
[add_group G]
[topological_space G]
[topological_add_group G]
[t2_space G]
{H : add_subgroup G}
[discrete_topology ↥H] :
@[protected, instance]
def
subgroup.is_closed_of_discrete
{G : Type u_1}
[group G]
[topological_space G]
[topological_group G]
[t2_space G]
{H : subgroup G}
[discrete_topology ↥H] :
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 ι) :
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 α) :
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 α) :
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 ι) :
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 ι) :
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 α) :
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 α) :
theorem
topological_add_comm_group_is_uniform
{G : Type u_1}
[add_comm_group G]
[topological_space G]
[topological_add_group G] :
theorem
topological_comm_group_is_uniform
{G : Type u_1}
[comm_group G]
[topological_space G]
[topological_group G] :
theorem
topological_add_group.t2_space_iff_zero_closed
{G : Type u_1}
[add_comm_group G]
[topological_space G]
[topological_add_group G] :
theorem
topological_group.t2_space_iff_one_closed
{G : Type u_1}
[comm_group G]
[topological_space G]
[topological_group G] :
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)) :
t2_space G
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)) :
t2_space G
theorem
uniform_add_group.to_uniform_space_eq
{G : Type u_1}
[u : uniform_space G]
[add_group G]
[uniform_add_group G] :
theorem
uniform_group.to_uniform_space_eq
{G : Type u_1}
[u : uniform_space G]
[group G]
[uniform_group G] :
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₀ : α) :
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₀ : α) :
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)) :
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]
def
quotient_group.complete_space'
(G : Type u)
[group G]
[topological_space G]
[topological_group G]
[topological_space.first_countable_topology G]
(N : subgroup G)
[N.normal]
[complete_space G] :
complete_space (G ⧸ N)
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]
def
quotient_add_group.complete_space'
(G : Type u)
[add_group G]
[topological_space G]
[topological_add_group G]
[topological_space.first_countable_topology G]
(N : add_subgroup G)
[N.normal]
[complete_space G] :
complete_space (G ⧸ N)
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]
def
quotient_group.complete_space
(G : Type u)
[group G]
[us : uniform_space G]
[uniform_group G]
[topological_space.first_countable_topology G]
(N : subgroup G)
[N.normal]
[hG : complete_space G] :
complete_space (G ⧸ N)
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]
def
quotient_add_group.complete_space
(G : Type u)
[add_group G]
[us : uniform_space G]
[uniform_add_group G]
[topological_space.first_countable_topology G]
(N : add_subgroup G)
[N.normal]
[hG : complete_space G] :
complete_space (G ⧸ N)
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.