Commit 2023-02-24 08:05 dfbcc376

View on Github →

feat: Port SetTheory.Ordinal.CantorNormalForm (#2471)

Estimated changes

added def Ordinal.CNF
added theorem Ordinal.CNFRec_pos
added theorem Ordinal.CNFRec_zero
added theorem Ordinal.CNF_foldr
added theorem Ordinal.CNF_fst_le
added theorem Ordinal.CNF_fst_le_log
added theorem Ordinal.CNF_lt_snd
added theorem Ordinal.CNF_ne_zero
added theorem Ordinal.CNF_of_le_one
added theorem Ordinal.CNF_of_lt
added theorem Ordinal.CNF_snd_lt
added theorem Ordinal.CNF_sorted
added theorem Ordinal.CNF_zero
added theorem Ordinal.one_CNF
added theorem Ordinal.zero_CNF