Commit 2024-10-10 02:53 6a2ce948

View on Github →

chore(SetTheory/Ordinal/Basic): golf various instances (#17527)

Estimated changes

added theorem InitialSeg.inj
added theorem Ordinal.inductionOn₂
added theorem Ordinal.inductionOn₃