Theorems · Definition · logic and foundations

Ordinal.nfp

(Ordinal.{u_1} → Ordinal.{u_1}) → Ordinal.{u_1} → Ordinal.{u_1}

The next fixed point function, the least fixed point of the normal function f, at least a. This is defined as nfpFamily applied to a family consisting only of f.

Defined in

Mathlib.SetTheory.Ordinal.FixedPoint

Cited by

41 results in Mathlib

Foundations

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