Commit 2026-04-05 15:16 de05f210

View on Github →

feat(SetTheory/Ordinal/FixedPointApproximants): add zero and limit lemmas for approximants (#37375) Add helper lemmas lfpApprox_zero, lfpApprox_limit, and the corresponding gfpApprox lemmas by duality.

Estimated changes

Modified Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean

added theorem OrdinalApprox.apply_lfpApprox_le_lfpApprox_of_lt

modified theorem OrdinalApprox.gfpApprox_eq_of_mem_fixedPoints

added theorem OrdinalApprox.gfpApprox_le_apply_gfpApprox_of_lt

added theorem OrdinalApprox.gfpApprox_of_isSuccLimit

added theorem OrdinalApprox.gfpApprox_zero

modified theorem OrdinalApprox.lfpApprox_eq_of_mem_fixedPoints

modified theorem OrdinalApprox.lfpApprox_mono_left

added theorem OrdinalApprox.lfpApprox_of_isSuccLimit

added theorem OrdinalApprox.lfpApprox_zero