rec_zero — Mathlib

English

The base case of the iterate recursion yields the starting value: Iterate.rec motive arg app 0 = arg.

Русский

Базовый случай рекурсии итераций даёт исходное значение: Iterate.rec motive arg app 0 = arg.

LaTeX

$$$$\mathrm{Iterate.rec}\ \text{motive}\ \text{arg}\ \text{app}\ 0 = \text{arg}. $$$$

Lean4

theorem rec_zero (motive : α → Sort*) {f : α → α} (app : ∀ a, motive a → motive (f a)) {a : α} (arg : motive a) :
    Iterate.rec motive arg app 0 = arg :=
  rfl

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