dist_eq_sub_of_le

Mathlib.Data.Nat.Dist

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

English

If n ≤ m, then the distance between n and m equals m − n.

Русский

Если n ≤ m, то расстояние между n и m равно m − n.

LaTeX

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

Lean4

theorem dist_eq_sub_of_le {n m : ℕ} (h : n ≤ m) : dist n m = m - n := by rw [dist, tsub_eq_zero_iff_le.mpr h, zero_add]

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

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

Разделы

Аффилиация

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