le_iff_eq_or_le_pred — Mathlib

English

For all a,b, a ≤ b iff a = b or a ≤ pred b (with appropriate assumptions).

Русский

Для любых a,b: a ≤ b эквивалентно a = b или a ≤ pred b (при соответствующих предпосылках).

LaTeX

$$$$a \le b \iff a = b \lor a \le pred(b).$$$$

Lean4

theorem le_iff_eq_or_le_pred : a ≤ b ↔ a = b ∨ a ≤ pred b :=
  by
  by_cases hb : IsMin b
  · simpa [hb.pred_eq] using le_of_eq
  · rw [le_pred_iff_of_not_isMin hb, le_iff_eq_or_lt]

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