Theorem Ordinal.CNF.snd_lt

Modification history

2025-08-18 23:36

Mathlib/SetTheory/Ordinal/CantorNormalForm.lean

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

Added Ordinal.CNF.snd_lt View on Github →