Commit 2024-09-24 06:31 1558c09c

View on Github →

chore(SetTheory/Ordinal/Basic): lift.initialSeg → liftInitialSeg (#16995)

Estimated changes

Modified Mathlib/SetTheory/Ordinal/Basic.lean

deleted def Ordinal.lift.initialSeg

modified theorem Ordinal.lift.initialSeg_coe

deleted def Ordinal.lift.principalSeg

modified theorem Ordinal.lift.principalSeg_top

added def Ordinal.liftInitialSeg

added theorem Ordinal.liftInitialSeg_coe

added def Ordinal.liftPrincipalSeg

added theorem Ordinal.liftPrincipalSeg_coe

added theorem Ordinal.liftPrincipalSeg_top'

added theorem Ordinal.liftPrincipalSeg_top