isMin — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

protected theorem isMin (h : IsSuccPrelimit a) : IsMin a := fun b hb =>
  by
  revert h
  refine Succ.rec (fun _ => le_rfl) (fun c _ H hc => ?_) hb
  have := hc.isMax.succ_eq
  rw [this] at hc ⊢
  exact H hc

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