dist

Mathlib.Data.Nat.Dist

URI: https://scilib.ai/kg/mathlib#Nat.dist

English

The distance on natural numbers is defined by dist(n,m) = n − m + (m − n).

Русский

Расстояние между натуральными числами определяется как dist(n,m) = n − m + (m − n).

LaTeX

$$def dist(n,m) := n - m + (m - n)$$

Lean4

/-- Distance (absolute value of difference) between natural numbers. -/
def dist (n m : ℕ) :=
  n - m + (m - n)

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

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

Разделы

Аффилиация

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