Def Ordinal.lift.initialSeg

Modification history

2024-09-24 06:31

Mathlib/SetTheory/Ordinal/Basic.lean

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

Deleted Ordinal.lift.initialSeg View on Github →

2023-02-13 06:43

Mathlib/SetTheory/Ordinal/Basic.lean

feat: port SetTheory.Ordinal.Basic (#2217) …

Added Ordinal.lift.initialSeg View on Github →