Theorems · Definition · logic and foundations

Ordinal.derivFamily

{ι : Type u_1} → (ι → Ordinal.{u} → Ordinal.{u}) → Ordinal.{u} → Ordinal.{u}

The derivative of a family of normal functions is the sequence of their common fixed points. This is defined for all functions such that Ordinal.derivFamily_zero, Ordinal.derivFamily_succ, and Ordinal.derivFamily_limit are satisfied.

Defined in

Mathlib.SetTheory.Ordinal.FixedPoint

Cited by

18 results in Mathlib

Foundations

Depth 41 from the axioms · uses propext, Classical.choice, Quot.sound