deriv_succ — Mathlib

English

Let f be a function on ordinals. Then the derivative at succ o satisfies deriv f (succ o) = nfp f (succ (deriv f o)).

Русский

Пусть f — функция на ординалах. Тогда производная в succ o удовлетворяет равенству deriv f (succ o) = nfp f (succ (deriv f o)).

LaTeX

$$$$ \operatorname{deriv} f (\operatorname{succ} o) = \operatorname{nfp} f (\operatorname{succ}(\operatorname{deriv} f o)) $$$$

Lean4

@[simp]
theorem deriv_succ (f o) : deriv f (succ o) = nfp f (succ (deriv f o)) :=
  derivFamily_succ _ _

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