deriv_eq_enumOrd — Mathlib

English

For a normal f, deriv f equals the enumeration of the fixed points of f.

Русский

Для нормальной f производная f совпадает с перечислением фиксированных точек f.

LaTeX

$$$$ \operatorname{deriv} f = \operatorname{enumOrd}(\operatorname{fixedPoints} f) $$$$

Lean4

/-- `Ordinal.deriv` enumerates the fixed points of a normal function. -/
theorem deriv_eq_enumOrd (H : IsNormal f) : deriv f = enumOrd (Function.fixedPoints f) :=
  by
  convert derivFamily_eq_enumOrd fun _ : Unit => H
  exact (Set.iInter_const _).symm

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