dist_eq_intro

Mathlib.Data.Nat.Dist

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

← MathLib Explorer

English

If n+m = k+l, then dist(n,k) = dist(l,m).

Русский

Если n+m = k+l, то dist(n,k) = dist(l,m).

LaTeX

$$$$ n+m = k+l \Rightarrow dist(n,k) = dist(l,m). $$$$

Lean4

theorem dist_eq_intro {n m k l : ℕ} (h : n + m = k + l) : dist n k = dist l m :=
  calc
    dist n k = dist (n + m) (k + m) := by rw [dist_add_add_right]
    _ = dist (k + l) (k + m) := by rw [h]
    _ = dist l m := by rw [dist_add_add_left]

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

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

Разделы

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

Аффилиация

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