Theorem OrderIso.ordinalType_congr

Modification history

2026-06-03 11:16
Mathlib/SetTheory/Ordinal/Basic.lean
feat: a cofinal set has a cofinal subset of order type `(cof α).ord` (#39789)
Added OrderIso.ordinalType_congrView on Github →