Theorem Ordinal.CNF.fst_le_log

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