isMin_or_mem_range_succ_or_isSuccLimit

English

For any a, either a is minimal, or a belongs to the succ-range, or a is a succ-limit.

Русский

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

LaTeX

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

Lean4

theorem isMin_or_mem_range_succ_or_isSuccLimit (a) : IsMin a ∨ a ∈ range (succ : α → α) ∨ IsSuccLimit a :=
  by
  rw [IsSuccLimit]
  have := mem_range_succ_or_isSuccPrelimit a
  tauto

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