nndist_dist — Mathlib

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]

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