dist_add_add_left

Mathlib.Data.Nat.Dist

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

English

For all n,m,k ∈ ℕ, dist(k+n, k+m) = dist(n,m).

Русский

Для любых n,m,k ∈ ℕ верно: dist(k+n, k+m) = dist(n,m).

LaTeX

$$$$ \operatorname{dist}(k+n, k+m) = \operatorname{dist}(n,m). $$$$

Lean4

theorem dist_add_add_left (k n m : ℕ) : dist (k + n) (k + m) = dist n m := by rw [add_comm k n, add_comm k m];
  apply dist_add_add_right

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

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

Разделы

Аффилиация

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