Theorem Ordinal.lift.principalSeg_top

Modification history

2024-09-24 06:31

Mathlib/SetTheory/Ordinal/Basic.lean

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

Modified Ordinal.lift.principalSeg_top View on Github →

2023-02-13 06:43

Mathlib/SetTheory/Ordinal/Basic.lean

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

Added Ordinal.lift.principalSeg_top View on Github →