Commit 2024-10-31 11:06 b420b713

View on Github →

chore(SetTheory/Ordinal/CantorNormalForm): cleanup proofs (#16998) We golf a bunch of proofs, and perform formatting improvements. We also deprecate CNF_fst_le, which is a weaker (and IME no more convenient) form of CNF_fst_le_log.

Estimated changes

modified theorem Ordinal.CNF_foldr
modified theorem Ordinal.CNF_of_le_one
modified theorem Ordinal.CNF_of_lt
modified theorem Ordinal.one_CNF
modified theorem Ordinal.zero_CNF