pred_le_le_iff — Mathlib

English

pred a ≤ b and b ≤ a iff b = a or b = pred a.

Русский

pred a ≤ b и b ≤ a эквивалентно b = a или b = pred a.

LaTeX

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

Lean4

theorem pred_le_le_iff {a b : α} : pred a ≤ b ∧ b ≤ a ↔ b = a ∨ b = pred a :=
  by
  refine ⟨fun h => or_iff_not_imp_left.2 fun hba : b ≠ a => (le_pred_of_lt <| h.2.lt_of_ne hba).antisymm h.1, ?_⟩
  rintro (rfl | rfl)
  · exact ⟨pred_le b, le_rfl⟩
  · exact ⟨le_rfl, pred_le a⟩

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