recF_eq

Mathlib.Data.QPF.Univariate.Basic

URI: https://scilib.ai/kg/mathlib#QPF.recF_eq

Lean4

theorem recF_eq {α : Type _} (g : F α → α) (x : q.P.W) : recF g x = g (abs (q.P.map (recF g) x.dest)) :=
  by
  cases x
  rfl

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

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

Разделы

Аффилиация

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