dist_eq

Mathlib.Topology.Instances.Int

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

English

The distance between integers x and y equals the absolute value of their integer difference.

Русский

Расстояние между целыми x и y равно модулю разности x−y.

LaTeX

$$$\\mathrm{dist}_{\\mathbb{Z}}(x,y) = |x - y|$$$

Lean4

theorem dist_eq (x y : ℤ) : dist x y = |(x : ℝ) - y| :=
  rfl

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

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

Разделы

Аффилиация

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