Theorems · Theorem · logic and foundations

Ordinal.nfpFamily_fp

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

Defined in

Mathlib.SetTheory.Ordinal.FixedPoint

Cited by

4 results in Mathlib

Foundations

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

Assumes

Small