succ_le_succ_iff

Mathlib.Order.SuccPred.Basic

URI: https://scilib.ai/kg/mathlib#Order.succ_le_succ_iff

English

For all a,b, succ(a) ≤ succ(b) if and only if a ≤ b.

Русский

Для любых a,b верно: succ(a) ≤ succ(b) тогда и только если a ≤ b.

LaTeX

$$$\operatorname{succ} a \leq \operatorname{succ} b \iff a \leq b$$$

Lean4

theorem succ_le_succ_iff : succ a ≤ succ b ↔ a ≤ b := by simp

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

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

Разделы

Аффилиация

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