nndist_eq'

Mathlib.Topology.MetricSpace.Pseudo.Defs

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

English

The same equality holds with reversed subtraction: nndist x y = nnabs(y−x).

Русский

Тождество: nndist x y = nnabs(y−x).

LaTeX

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

Lean4

theorem nndist_eq' (x y : ℝ) : nndist x y = Real.nnabs (y - x) :=
  nndist_comm _ _

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

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

Разделы

Аффилиация

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