Theorems · Theorem · logic and foundations

Ordinal.fp_iff_derivFamily

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

Defined in

Mathlib.SetTheory.Ordinal.FixedPoint

Cited by

2 results in Mathlib

Foundations

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

Assumes

Small