le_succ_iff_eq_or_le

Mathlib.Data.Nat.SuccPred

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

English

For natural numbers, m ≤ n.succ is equivalent to m = n.succ or m ≤ n.

Русский

Для натуральных чисел m ≤ n+1 эквивалентно m = n+1 или m ≤ n.

LaTeX

$$$\\\\forall m,n \\\\in \\\\mathbb N, \\\\ m \\\\le \\\\ n.succ \\\\iff \\\\ m = n.succ \\\\lor \\\\ m \\\\le \\\\ n.$$$

Lean4

theorem le_succ_iff_eq_or_le : m ≤ n.succ ↔ m = n.succ ∨ m ≤ n :=
  Order.le_succ_iff_eq_or_le

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

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

Разделы

Аффилиация

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