English
Definition of a recursive construction isSuccPrelimitRecOn: a value is built by either a given isSuccPrelimit or by transporting along a witness from not-isSuccPrelimit.
Русский
Определение isSuccPrelimitRecOn: значение строится либо по данным isSuccPrelimit, либо переносом вдоль свидетеля из not-isSuccPrelimit.
LaTeX
$$isSuccPrelimitRecOn : motive\\ b = \\begin{cases} isSuccPrelimit\\ b\\ hb, & \\text{if } hb : IsSuccPrelimit b \\\\ cast (congr_arg\\ motive\\ H) (succ\\ _ H_1), & \\text{otherwise} \\end{cases}$$
Lean4
/-- A value can be built by building it on successors and successor pre-limits. -/
@[elab_as_elim]
noncomputable def isSuccPrelimitRecOn : motive b :=
if hb : IsSuccPrelimit b then isSuccPrelimit b hb
else
haveI H := Classical.choose_spec (not_isSuccPrelimit_iff.1 hb)
cast (congr_arg motive H.2) (succ _ H.1)
