Commit 2024-12-02 16:40 ceca1670

View on Github →

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

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Aleph.lean

modified theorem Cardinal.type_cardinal

Modified Mathlib/SetTheory/Ordinal/Basic.lean

modified theorem Ordinal.lift.principalSeg_top'

modified theorem Ordinal.liftPrincipalSeg_top'

modified theorem Ordinal.type_fin

modified theorem Ordinal.type_lt

modified theorem Ordinal.type_nat_lt

modified theorem Ordinal.type_toType

modified theorem Ordinal.univ_id