abs_dist

Mathlib.Topology.MetricSpace.Pseudo.Defs

URI: https://scilib.ai/kg/mathlib#abs_dist

English

The distance is nonnegative and equals its absolute value: |dist x y| = dist x y.

Русский

Расстояние неотрицательно и равно своему абсолютному значению: |dist x y| = dist x y.

LaTeX

$$|dist(x,y)| = dist(x,y)$$

Lean4

@[simp]
theorem abs_dist {a b : α} : |dist a b| = dist a b :=
  abs_of_nonneg dist_nonneg

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

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

Разделы

Аффилиация

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