Theorem Cardinal.mk_Iio_ord_out_α

Modification history

2024-08-27 18:38

Mathlib/SetTheory/Ordinal/Basic.lean

chore(SetTheory/Ordinal/*): `o.out.α` → `o.toType` (#16161) …

Deleted Cardinal.mk_Iio_ord_out_α View on Github →

2024-05-21 16:45

Mathlib/SetTheory/Ordinal/Basic.lean

feat: SuccOrder and recursion principle on well-ordered type (#11290) …

Added Cardinal.mk_Iio_ord_out_α View on Github →