Commit 2026-04-05 08:48 301c8f7f

View on Github →

chore(SetTheory/Ordinal/FixedPointApproximants): simpler definition for lfpApprox (#37383) We simplify the definition of Ordinal.lfpApprox - the old definition wasn't even simp-normal. We then golf the entire API using it.

Estimated changes

Modified Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean

modified theorem OrdinalApprox.gfpApprox_add_one

added theorem OrdinalApprox.gfpApprox_anti_right

deleted theorem OrdinalApprox.gfpApprox_antitone

modified theorem OrdinalApprox.gfpApprox_eq_of_mem_fixedPoints

modified theorem OrdinalApprox.gfpApprox_ord_mem_fixedPoint

modified theorem OrdinalApprox.lfpApprox_add_one

modified theorem OrdinalApprox.lfpApprox_eq_of_mem_fixedPoints

modified theorem OrdinalApprox.lfpApprox_mem_fixedPoints_of_eq

modified theorem OrdinalApprox.lfpApprox_mono_left

added theorem OrdinalApprox.lfpApprox_mono_right

deleted theorem OrdinalApprox.lfpApprox_monotone

modified theorem OrdinalApprox.lfpApprox_ord_mem_fixedPoint