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 #
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_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)
@[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.
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)
@[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 : α) :
theorem
uniformity_translate_mul
{α : Type u_1}
[uniform_space α]
[group α]
[uniform_group α]
(a : α) :
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
uniformity_eq_comap_nhds_zero
(α : Type u_1)
[uniform_space α]
[add_group α]
[uniform_add_group α] :
theorem
uniformity_eq_comap_nhds_one_swapped
(α : Type u_1)
[uniform_space α]
[group α]
[uniform_group α] :
theorem
uniformity_eq_comap_nhds_zero_swapped
(α : Type u_1)
[uniform_space α]
[add_group α]
[uniform_add_group α] :
theorem
uniformity_eq_comap_inv_mul_nhds_one
(α : Type u_1)
[uniform_space α]
[group α]
[uniform_group α] :
theorem
uniformity_eq_comap_neg_add_nhds_zero
(α : Type u_1)
[uniform_space α]
[add_group α]
[uniform_add_group α] :
theorem
uniformity_eq_comap_neg_add_nhds_zero_swapped
(α : Type u_1)
[uniform_space α]
[add_group α]
[uniform_add_group α] :
theorem
uniformity_eq_comap_inv_mul_nhds_one_swapped
(α : Type u_1)
[uniform_space α]
[group α]
[uniform_group α] :
theorem
filter.has_basis.uniformity_of_nhds_one
{α : Type u_1}
[uniform_space α]
[group α]
[uniform_group α]
{ι : Sort u_2}
{p : ι → Prop}
{U : ι → set α}
(h : (𝓝 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 : (𝓝 0).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 : (𝓝 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 : (𝓝 1).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 (𝓝 1) (𝓝 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 (𝓝 0) (𝓝 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) :
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) :
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
totally_bounded_iff_subset_finite_Union_nhds_zero
{α : Type u_1}
[uniform_space α]
[add_group α]
[uniform_add_group α]
{s : set α} :
theorem
totally_bounded_iff_subset_finite_Union_nhds_one
{α : Type u_1}
[uniform_space α]
[group α]
[uniform_group α]
{s : set α} :
def
topological_add_group.to_uniform_space
(G : Type u_1)
[add_comm_group G]
[topological_space G]
[topological_add_group G] :
The right uniformity on a topological group
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) (𝓝 0), refl := _, symm := _, comp := _}, is_open_uniformity := _}
def
topological_group.to_uniform_space
(G : Type u_1)
[comm_group G]
[topological_space G]
[topological_group G] :
The right uniformity on a topological group.
Equations
- topological_group.to_uniform_space G = {to_topological_space := _inst_2, to_core := {uniformity := filter.comap (λ (p : G × G), p.snd / p.fst) (𝓝 1), refl := _, symm := _, comp := _}, is_open_uniformity := _}
theorem
topological_group.tendsto_uniformly_iff
{G : Type u_1}
[comm_group G]
[topological_space G]
[topological_group G]
{ι : Type u_2}
{α : Type u_3}
(F : ι → α → G)
(f : α → G)
(p : filter ι) :
theorem
topological_add_group.tendsto_uniformly_iff
{G : Type u_1}
[add_comm_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_comm_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}
[comm_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_comm_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}
[comm_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}
[comm_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_comm_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
uniformity_eq_comap_nhds_zero'
(G : Type u_1)
[add_comm_group G]
[topological_space G]
[topological_add_group G] :
theorem
uniformity_eq_comap_nhds_one'
(G : Type u_1)
[comm_group G]
[topological_space G]
[topological_group G] :
theorem
topological_group_is_uniform
{G : Type u_1}
[comm_group G]
[topological_space G]
[topological_group G] :
theorem
topological_add_group_is_uniform
{G : Type u_1}
[add_comm_group G]
[topological_space G]
[topological_add_group G] :
theorem
topological_group.separated_iff_one_closed
{G : Type u_1}
[comm_group G]
[topological_space G]
[topological_group G] :
separated_space G ↔ is_closed {1}
theorem
topological_add_group.separated_iff_zero_closed
{G : Type u_1}
[add_comm_group G]
[topological_space G]
[topological_add_group G] :
separated_space G ↔ is_closed {0}
theorem
topological_group.separated_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 ∈ 𝓝 1), x ∉ U)) :
theorem
topological_add_group.separated_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 ∈ 𝓝 0), x ∉ U)) :
theorem
uniform_add_group.to_uniform_space_eq
{G : Type u_1}
[u : uniform_space G]
[add_comm_group G]
[uniform_add_group G] :
theorem
uniform_group.to_uniform_space_eq
{G : Type u_1}
[u : uniform_space G]
[comm_group G]
[uniform_group G] :
theorem
tendsto_div_comap_self
{α : Type u_1}
{β : Type u_2}
{hom : Type u_3}
[topological_space α]
[comm_group α]
[topological_group α]
[topological_space β]
[comm_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_comm_group α]
[topological_add_group α]
[topological_space β]
[add_comm_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.