Theorems · Theorem · logic and foundations

Ordinal.derivFamily_eq_enumOrd

∀ {ι : Type u_1} {f : ι → Ordinal.{u} → Ordinal.{u}} [Small.{u, u_1} ι],
  (∀ (i : ι), Order.IsNormal (f i)) → Ordinal.derivFamily f = Ordinal.enumOrd (⋂ i, Function.fixedPoints (f i))

For a family of normal functions, Ordinal.derivFamily enumerates the common fixed points.

Defined in

Mathlib.SetTheory.Ordinal.FixedPoint

Cited by

2 results in Mathlib

Foundations

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

Assumes

Small