Theorem OrdinalApprox.gfpApprox_of_isSuccLimit

Modification history

2026-04-05 15:16
Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean
feat(SetTheory/Ordinal/FixedPointApproximants): add zero and limit lemmas for approximants (#37375) …
Added OrdinalApprox.gfpApprox_of_isSuccLimitView on Github →