Commit 2024-10-11 15:01 25d20576

View on Github →

feat(SetTheory/Cardinal/Basic): Cardinal.liftInitialSeg (#16958) We introduce an InitialSeg version of Cardinal.lift and use it to golf down the lift API.

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Basic.lean

added def Cardinal.liftInitialSeg

modified theorem Cardinal.lift_le

added theorem Cardinal.mem_range_of_le_lift

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

Modified Mathlib/SetTheory/Ordinal/Basic.lean