limitRecOn_limit — Mathlib

English

Bounded recursion principle for limit ordinals: given a motive, the limit-case equals the specified bound expression.

Русский

Принцип ограниченной рекурсии для пределов: ограниченная по пределу часть равна заданному выражению границы.

LaTeX

$$$\forall motive\ o\ H_1\ H_2\ H_3\ h,\ \mathrm{limitRecOn}(o, H_1, H_2, H_3) = H_3\ o\ h\ (\lambda x\, \_h, \mathrm{limitRecOn} x\ H_1 H_2 H_3)$$$

Lean4

@[simp]
theorem limitRecOn_limit {motive} (o H₁ H₂ H₃ h) :
    @limitRecOn motive o H₁ H₂ H₃ = H₃ o h fun x _h => @limitRecOn motive x H₁ H₂ H₃ :=
  SuccOrder.limitRecOn_of_isSuccLimit ..

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