Theorems · Theorem · logic and foundations

Ordinal.derivFamily_fp

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

Defined in

Mathlib.SetTheory.Ordinal.FixedPoint

Cited by

3 results in Mathlib

Foundations

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

Assumes

Small