Theorem Cardinal.nonempty_ord_toType

Modification history

2026-07-03 08:36
Mathlib/SetTheory/Ordinal/Basic.lean
feat(CategoryTheory/Presentable): sharply smaller regular cardinals (#40937) …
Added Cardinal.nonempty_ord_toTypeView on Github →