dist_eq_zero

Mathlib.Data.Nat.Dist

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

English

Let n and m be natural numbers. If n = m, then the distance between n and m is 0.

Русский

Пусть n и m — натуральные числа. Если n = m, то расстояние между n и m равно 0.

LaTeX

$$$n = m \Rightarrow \operatorname{dist}(n,m) = 0$$$

Lean4

theorem dist_eq_zero {n m : ℕ} (h : n = m) : dist n m = 0 := by rw [h, dist_self]

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

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

Разделы

Аффилиация

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