pred_le_iff_eq_or_le — Mathlib

English

For any a,b, pred a ≤ b is equivalent to either b = pred a or a ≤ b.

Русский

Для любых a,b pred a ≤ b эквивалентно либо b = pred a, либо a ≤ b.

LaTeX

$$$\operatorname{pred} a \le b \iff (b = \operatorname{pred} a) \lor (a \le b)$$$

Lean4

theorem pred_le_iff_eq_or_le : pred a ≤ b ↔ b = pred a ∨ a ≤ b :=
  by
  by_cases ha : IsMin a
  · rw [ha.pred_eq, or_iff_right_of_imp ge_of_eq]
  · rw [← pred_lt_iff_of_not_isMin ha, le_iff_eq_or_lt, eq_comm]

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