Theorem OrdinalApprox.gfpApprox_le_apply_gfpApprox_of_lt

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_le_apply_gfpApprox_of_ltView on Github →