dist_comm

Mathlib.Data.Nat.Dist

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

English

Distance is symmetric: dist(n,m) = dist(m,n).

Русский

Расстояние симметрично: dist(n,m) = dist(m,n).

LaTeX

$$dist(n,m) = dist(m,n)$$

Lean4

theorem dist_comm (n m : ℕ) : dist n m = dist m n := by simp [dist, add_comm]

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

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

Разделы

Аффилиация

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