prelimitRecOn — Mathlib

English

If b is minimal, the limit recursion reduces to isMin at b.

Русский

Если b минимален, предел-рекурсия сводится к isMin(b).

LaTeX

$$$\\mathrm{isSuccLimitRecOn}(b, isMin, succ, isSuccLimit) = \\mathrm{isMin}(b, hb)$ for $hb: IsMin(b).$$$

Lean4

/-- Recursion principle on a well-founded partial `SuccOrder`. -/
@[elab_as_elim]
noncomputable def prelimitRecOn : motive b :=
  wellFounded_lt.fix
    (fun a IH ↦
      if h : IsSuccPrelimit a then isSuccPrelimit a h IH
      else
        haveI H := Classical.choose_spec (not_isSuccPrelimit_iff.1 h)
        cast (congr_arg motive H.2) (succ _ H.1 <| IH _ <| H.2.subst <| lt_succ_of_not_isMax H.1))
    b

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