uniformSpace_edist — Mathlib

English

The uniform space induced by edist coincides with the given pseudo-emetric space structure.

Русский

Уравнивается структура равномерности, порождённая edist, с заданной псевдо-эмитрической структурой.

LaTeX

$$$ ‹PseudoEMetricSpace\ α›.toUniformSpace = uniformSpaceOfEDist\ edist\ edist\_self\ edist\_comm\ edist\_triangle $$$

Lean4

theorem uniformSpace_edist :
    ‹PseudoEMetricSpace α›.toUniformSpace = uniformSpaceOfEDist edist edist_self edist_comm edist_triangle :=
  UniformSpace.ext uniformity_pseudoedist

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