dist_eq

Mathlib.Topology.MetricSpace.Pseudo.Constructions

URI: https://scilib.ai/kg/mathlib#NNReal.dist_eq

English

In NNReal, the distance between a and b equals the absolute difference of their real values: dist a b = |a - b| with a,b interpreted in ℝ≥0.

Русский

В NNReal расстояние между a и b равно модулю разности их вещественных значений.

LaTeX

$$$\\operatorname{dist} a b = |(a: \\mathbb{R}) - b|$$$

Lean4

theorem dist_eq (a b : ℝ≥0) : dist a b = |(a : ℝ) - b| :=
  rfl

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

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

Разделы

Аффилиация

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