English
Two pseudo-emetric structures coincide when their edge-distance (edist) is the same; equivalently, the uniform structure is determined by edist.
Русский
Две псевдо-эмитрические структуры совпадают, если равны их edist; структура uniforme определяется edist.
LaTeX
$$$ m.toEDist = m'.toEDist \Rightarrow m = m' $$$
Lean4
/-- Creating a uniform space from an extended distance. -/
@[reducible]
def uniformSpaceOfEDist (edist : α → α → ℝ≥0∞) (edist_self : ∀ x : α, edist x x = 0)
(edist_comm : ∀ x y : α, edist x y = edist y x) (edist_triangle : ∀ x y z : α, edist x z ≤ edist x y + edist y z) :
UniformSpace α :=
.ofFun edist edist_self edist_comm edist_triangle fun ε ε0 =>
⟨ε / 2, ENNReal.half_pos ε0.ne', fun _ h₁ _ h₂ => (ENNReal.add_lt_add h₁ h₂).trans_eq (ENNReal.add_halves _)⟩
