le_le_succ_iff — Mathlib

English

a ≤ b and b ≤ succ a if and only if b = a or b = succ a.

Русский

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

LaTeX

$$a \le b \land b \le succ a \iff b = a \lor b = succ a$$

Lean4

theorem le_le_succ_iff : a ≤ b ∧ b ≤ succ a ↔ b = a ∨ b = succ a :=
  by
  refine
    ⟨fun h => or_iff_not_imp_left.2 fun hba : b ≠ a => h.2.antisymm (succ_le_of_lt <| h.1.lt_of_ne <| hba.symm), ?_⟩
  rintro (rfl | rfl)
  · exact ⟨le_rfl, le_succ b⟩
  · exact ⟨le_succ a, le_rfl⟩

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