Commit 2024-10-19 07:30 61509b3d

View on Github →

chore(SetTheory/Ordinal/Basic): make Ordinal.typein a PrincipalSeg (#17599) This allows us to golf most of its API down to one-liners.

Estimated changes

Modified Mathlib/Order/InitialSeg.lean

added theorem PrincipalSeg.surjOn

Modified Mathlib/SetTheory/Ordinal/Basic.lean

added theorem Ordinal.mem_range_typein_iff

added theorem Ordinal.top_typein

added theorem Ordinal.type_subrel

deleted def Ordinal.typein.principalSeg

modified def Ordinal.typein

added theorem Ordinal.typein_surjOn

modified theorem Ordinal.typein_top