Theorem Ordinal.CNF.lt_snd

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.lt_snd View on Github →