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