Commit 2025-08-18 23:36 ea164ea5

View on Github →

chore(SetTheory/Ordinal/CantorNormalForm): namespace results on the CNF (#28584)

Estimated changes

added theorem Ordinal.CNF.fst_le_log
added theorem Ordinal.CNF.lt_snd
added theorem Ordinal.CNF.rec_pos
added theorem Ordinal.CNF.rec_zero
added theorem Ordinal.CNF.snd_lt
added theorem Ordinal.CNF.zero_right
modified def Ordinal.CNF
deleted theorem Ordinal.CNFRec_pos
deleted theorem Ordinal.CNFRec_zero
deleted theorem Ordinal.CNF_foldr
deleted theorem Ordinal.CNF_fst_le_log
deleted theorem Ordinal.CNF_lt_snd
deleted theorem Ordinal.CNF_ne_zero
deleted theorem Ordinal.CNF_of_le_one
deleted theorem Ordinal.CNF_of_lt
deleted theorem Ordinal.CNF_snd_lt
deleted theorem Ordinal.CNF_sorted
deleted theorem Ordinal.CNF_zero
deleted theorem Ordinal.one_CNF
deleted theorem Ordinal.zero_CNF