rec

Mathlib.Logic.Function.Iterate

URI: https://scilib.ai/kg/mathlib#Function.Iterate.rec

Lean4

/-- A recursor for the iterate of a function. -/
@[elab_as_elim]
def rec (motive : α → Sort*) {a : α} (arg : motive a) {f : α → α} (app : ∀ a, motive a → motive (f a)) (n : ℕ) :
    motive (f^[n] a) :=
  match n with
  | 0 => arg
  | m + 1 => Iterate.rec motive (app _ arg) app m

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru