Theorem OrdinalApprox.apply_lfpApprox_le_lfpApprox_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.apply_lfpApprox_le_lfpApprox_of_ltView on Github →