mem_range_succ_or_isSuccPrelimit — Mathlib

English

For any a, either a is in the range of succ or a is a succ-prelimit.

Русский

Для любого a либо a лежит в образе succ, либо a является succ-предпредельным.

LaTeX

$$$\forall a:\alpha,\ a \in \operatorname{range}(\mathrm{succ}) \lor IsSuccPrelimit(a)$$$

Lean4

theorem mem_range_succ_or_isSuccPrelimit (a) : a ∈ range (succ : α → α) ∨ IsSuccPrelimit a :=
  or_iff_not_imp_right.2 <| mem_range_succ_of_not_isSuccPrelimit

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