eq_of_dist_eq_zero

Mathlib.Data.Nat.Dist

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

← MathLib Explorer

English

If dist(n,m) = 0, then n = m.

Русский

Если dist(n,m) = 0, то n = m.

LaTeX

$$dist(n,m) = 0 \Rightarrow n = m$$

Lean4

theorem eq_of_dist_eq_zero {n m : ℕ} (h : dist n m = 0) : n = m :=
  have : n - m = 0 := Nat.eq_zero_of_add_eq_zero_right h
  have : n ≤ m := tsub_eq_zero_iff_le.mp this
  have : m - n = 0 := Nat.eq_zero_of_add_eq_zero_left h
  have : m ≤ n := tsub_eq_zero_iff_le.mp this
  le_antisymm ‹n ≤ m› ‹m ≤ n›

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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