succ_eq_succ_iff_of_not_isMax — Mathlib

English

If a and b are not maximal, then succ a = succ b if and only if a = b; i.e., successor is injective on non-maximal elements.

Русский

Если ни a ни b не являются максимальными, то succ a = succ b тогда и только если a = b; то есть переход к следующему элементу является инъективным на немаксимальных элементах.

LaTeX

$$$\neg\IsMax(a) \land \neg\IsMax(b) \Rightarrow (\operatorname{succ} a = \operatorname{succ} b \iff a = b)$$$

Lean4

theorem succ_eq_succ_iff_of_not_isMax (ha : ¬IsMax a) (hb : ¬IsMax b) : succ a = succ b ↔ a = b := by
  rw [eq_iff_le_not_lt, eq_iff_le_not_lt, succ_le_succ_iff_of_not_isMax ha hb, succ_lt_succ_iff_of_not_isMax ha hb]

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