nndist_eq

Mathlib.Topology.MetricSpace.Pseudo.Defs

URI: https://scilib.ai/kg/mathlib#Real.nndist_eq

English

For real numbers x,y, the nonnegative distance nndist equals nnabs(x−y).

Русский

Для чисел x,y неотрицательная дистанция nndist равна nnabs(x−y).

LaTeX

$$$\\operatorname{nndist}(x,y) = \\operatorname{Real.nnabs}(x-y)$ for all x,y ∈ ℝ.$$

Lean4

theorem nndist_eq (x y : ℝ) : nndist x y = Real.nnabs (x - y) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru