Theorem Ordinal.liftPrincipalSeg_top'

Modification history

2024-12-02 16:40

Mathlib/SetTheory/Ordinal/Basic.lean

feat(SetTheory/Ordinal/Basic): notation `typeLT α = type (α := α) (· < ·)` (#18235)

Modified Ordinal.liftPrincipalSeg_top'View on Github →

2024-09-24 06:31

Mathlib/SetTheory/Ordinal/Basic.lean

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

Added Ordinal.liftPrincipalSeg_top'View on Github →