dist_tri_right'

Mathlib.Data.Nat.Dist

URI: https://scilib.ai/kg/mathlib#Nat.dist_tri_right'

English

For all natural numbers n and m, we have n ≤ m + dist(n,m).

Русский

Для любых натуральных чисел n и m выполняется n ≤ m + dist(n,m).

LaTeX

$$$n \le m + \operatorname{dist}(n,m)$$$

Lean4

theorem dist_tri_right' (n m : ℕ) : n ≤ m + dist n m := by rw [dist_comm]; apply dist_tri_right

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

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

Разделы

Аффилиация

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