deriv_zero_right — Mathlib

English

Let f be a function from ordinals to ordinals. Then the derivative at 0 equals the least fixed point of f.

Русский

Пусть f — функция от ординалов в ординалы. Тогда производная в нуле равна наименьшей фиксированной точке функции f.

LaTeX

$$$$ \operatorname{deriv}(f)(0) = \operatorname{nfp}(f)(0) $$$$

Lean4

@[simp]
theorem deriv_zero_right (f) : deriv f 0 = nfp f 0 :=
  derivFamily_zero _

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