dist_eq_sub_of_le_right

Mathlib.Data.Nat.Dist

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

English

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

Русский

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

LaTeX

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

Lean4

theorem dist_eq_sub_of_le_right {n m : ℕ} (h : m ≤ n) : dist n m = n - m := by rw [dist_comm]; apply dist_eq_sub_of_le h

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

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

Разделы

Аффилиация

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