# mathlibdocumentation

topology.algebra.uniform_group

# Uniform structure on topological groups #

• topological_add_group.to_uniform_space and topological_add_group_is_uniform can be used to construct a canonical uniformity for a topological add group.

• extension of ℤ-bilinear maps to complete groups (useful for ring completions)

• add_group_with_zero_nhd: construct the topological structure from a group with a neighbourhood around zero. Then with topological_add_group.to_uniform_space one can derive a uniform_space.

@[class]
Prop

A uniform (additive) group is a group in which the addition and negation are uniformly continuous.

Instances
theorem uniform_add_group.mk' {α : Type u_1} [add_group α] (h₁ : uniform_continuous (λ (p : α × α), p.fst + p.snd)) (h₂ : uniform_continuous (λ (p : α), -p)) :
theorem uniform_continuous_sub {α : Type u_1} [add_group α]  :
uniform_continuous (λ (p : α × α), p.fst - p.snd)
theorem uniform_continuous.sub {α : Type u_1} {β : Type u_2} [add_group α] {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} [add_group α] {f : β → α} (hf : uniform_continuous f) :
uniform_continuous (λ (x : β), -f x)
theorem uniform_continuous_neg {α : Type u_1} [add_group α]  :
uniform_continuous (λ (x : α), -x)
theorem uniform_continuous.add {α : Type u_1} {β : Type u_2} [add_group α] {f g : β → α} (hf : uniform_continuous f) (hg : uniform_continuous g) :
uniform_continuous (λ (x : β), f x + g x)
uniform_continuous (λ (p : α × α), p.fst + p.snd)
@[instance]
@[instance]
theorem uniformity_translate {α : Type u_1} [add_group α] (a : α) :
filter.map (λ (x : α × α), (x.fst + a, x.snd + a)) (𝓤 α) = 𝓤 α
theorem uniform_embedding_translate {α : Type u_1} [add_group α] (a : α) :
uniform_embedding (λ (x : α), x + a)
theorem uniformity_eq_comap_nhds_zero (α : Type u_1) [add_group α]  :
𝓤 α = filter.comap (λ (x : α × α), x.snd - x.fst) (𝓝 0)
theorem group_separation_rel {α : Type u_1} [add_group α] (x y : α) :
(x, y) 𝓢 α x - y closure {0}
theorem uniform_continuous_of_tendsto_zero {α : Type u_1} {β : Type u_2} [add_group α] [add_group β] {f : α →+ β} (h : (𝓝 0) (𝓝 0)) :
theorem add_monoid_hom.uniform_continuous_of_continuous_at_zero {α : Type u_1} {β : Type u_2} [add_group α] [add_group β] (f : α →+ β) (hf : 0) :
theorem uniform_continuous_of_continuous {α : Type u_1} {β : Type u_2} [add_group α] [add_group β] {f : α →+ β} (h : continuous f) :

The right uniformity on a topological group.

Equations
theorem uniformity_eq_comap_nhds_zero' (G : Type u)  :
𝓤 G = filter.comap (λ (p : G × G), p.snd - p.fst) (𝓝 0)
theorem topological_add_group_is_uniform {G : Type u}  :
theorem to_uniform_space_eq {G : Type u} [u : uniform_space G]  :
theorem tendsto_sub_comap_self {α : Type u_1} {β : Type u_2} {e : β →+ α} (de : dense_inducing e) (x₀ : α) :
filter.tendsto (λ (t : β × β), t.snd - t.fst) (filter.comap (λ (p : β × β), (e p.fst, e p.snd)) (𝓝 (x₀, x₀))) (𝓝 0)
theorem dense_inducing.extend_Z_bilin {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {G : Type u_5} {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.