English
From a pseudometric space with edistance finite everywhere, push the edistance to a real-valued distance dist that agrees with edist via toReal, thus obtaining a pseudometric space whose distance function is dist and whose edist matches the original.
Русский
Из псевдометрического пространства с конечной повсеместной edist переводим edist в действительную функцию расстояния dist, согласующуюся с edist через toReal, получая псевдометрическое пространство, где расстояние равно dist, а edist сохраняется.
LaTeX
$$$\\text{If } (α, e) \\text{ is PseudoEMetricSpace and dist: α×α→\\mathbb{R} \\text{ with } dist(x,y)=\\operatorname{toReal}(e.edist(x,y))\\text{ and } e.edist(x,y)\\neq \\top, \\text{ then } α$ endowed with dist is a PseudoMetricSpace with the same uniformity as given by $e$.$$
Lean4
/-- One gets a pseudometric space from an emetric space if the edistance
is everywhere finite, by pushing the edistance to reals. We set it up so that the edist and the
uniformity are defeq in the pseudometric space and the pseudoemetric space. In this definition, the
distance is given separately, to be able to prescribe some expression which is not defeq to the
push-forward of the edistance to reals. See note [reducible non-instances]. -/
abbrev toPseudoMetricSpaceOfDist {α : Type u} [e : PseudoEMetricSpace α] (dist : α → α → ℝ)
(edist_ne_top : ∀ x y : α, edist x y ≠ ⊤) (h : ∀ x y, dist x y = ENNReal.toReal (edist x y)) : PseudoMetricSpace α
where
dist := dist
dist_self x := by simp [h]
dist_comm x y := by simp [h, edist_comm]
dist_triangle x y
z := by
simp only [h]
exact ENNReal.toReal_le_add (edist_triangle _ _ _) (edist_ne_top _ _) (edist_ne_top _ _)
edist := edist
edist_dist _ _ := by simp only [h, ENNReal.ofReal_toReal (edist_ne_top _ _)]
toUniformSpace := e.toUniformSpace
uniformity_dist :=
e.uniformity_edist.trans <| by
simpa only [ENNReal.coe_toNNReal (edist_ne_top _ _), h] using
(Metric.uniformity_edist_aux fun x y : α => (edist x y).toNNReal).symm
