succ_lt — Mathlib

English

If IsSuccPrelimit(b) holds, then for any a < b, succ a < b.

Русский

Если IsSuccPrelimit(b) истинно, тогда для любого a < b выполнено succ a < b.

LaTeX

$$$\forall a:\alpha, \forall b:\alpha, IsSuccPrelimit(b) \land a < b \Rightarrow succ(a) < b$$$

Lean4

theorem succ_lt (hb : IsSuccPrelimit b) (ha : a < b) : succ a < b :=
  by
  by_cases h : IsMax a
  · rwa [h.succ_eq]
  · rw [lt_iff_le_and_ne, succ_le_iff_of_not_isMax h]
    refine ⟨ha, fun hab => ?_⟩
    subst hab
    exact (h hb.isMax).elim

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