dist_edist — Mathlib

English

Distance in α equals the real value of distance via edist: dist x y = (edist x y).toReal.

Русский

Расстояние в α равно действительному значению расстояния через edist: dist x y = (edist x y).toReal.

LaTeX

$$$ dist(x,y) = (edist(x,y)).toReal $$$

Lean4

/-- Express `dist` in terms of `edist` -/
theorem dist_edist (x y : α) : dist x y = (edist x y).toReal := by rw [edist_dist, ENNReal.toReal_ofReal dist_nonneg]

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