toUniformSpace_eq — Mathlib

English

The uniform space structure on R induced by Valued R Γ₀ coincides with the standard IsTopologicalAddGroup uniform space.

Русский

Структура униформности на R, задаваемая Valued R Γ₀, совпадает с обычной униформной структурой группы сложения.

LaTeX

$$$ toUniformSpace = IsTopologicalAddGroup.toUniformSpace(R)$$$

Lean4

theorem toUniformSpace_eq : toUniformSpace = @IsTopologicalAddGroup.toUniformSpace R _ v.subgroups_basis.topology _ :=
  UniformSpace.ext ((hasBasis_uniformity R Γ₀).eq_of_same_basis <| v.subgroups_basis.hasBasis_nhds_zero.comap _)

Похожие утверждения