toUniformSpace_eq — Mathlib

English

Let α be a type with a pseudometric. The uniform structure on α coming from the distance function dist coincides with the standard uniform structure on α.

Русский

Пусть α — множество с псевдометрикой. Униформная структура на α, полученная от расстояния dist, совпадает с обычной униформной структурой на α.

LaTeX

$$$$ \mathcal{U}(\alpha) = \mathrm{UniformSpace.ofDist}(\operatorname{dist}) $$$$

Lean4

theorem toUniformSpace_eq : ‹PseudoMetricSpace α›.toUniformSpace = .ofDist dist dist_self dist_comm dist_triangle :=
  UniformSpace.ext PseudoMetricSpace.uniformity_dist

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