succ_lt — Mathlib

English

If b is a succ-limit, then for any a < b, succ a < b, and conversely the same equivalence holds for IsSuccLimit.

Русский

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

LaTeX

$$$IsSuccLimit(b) \Rightarrow (a < b \Rightarrow succ(a) < b) \quad\text{and}\quad (a < b \Rightarrow succ(a) < b) \Rightarrow IsSuccLimit(b)$$

Lean4

theorem succ_lt (hb : IsSuccLimit b) (ha : a < b) : succ a < b :=
  hb.isSuccPrelimit.succ_lt ha

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