English
For any x,y in α, the nonnegative distance nndist is the NNReal corresponding to the real distance dist x y, i.e., nndist x y = Real.toNNReal (dist x y).
Русский
Для любых x,y ∈ α неотрицательное расстояние nndist равно соответствующему NNReal значению расстояния dist x y, то есть nndist x y = Real.toNNReal (dist x y).
LaTeX
$$$ nndist(x,y) = \operatorname{Real.toNNReal}(\operatorname{dist}(x,y)) $$$
Lean4
/-- Express `nndist` in terms of `dist` -/
theorem nndist_dist (x y : α) : nndist x y = Real.toNNReal (dist x y) := by rw [dist_nndist, Real.toNNReal_coe]