Theorem Cardinal.noMaxOrder

Modification history

2024-10-11 12:40

Mathlib/SetTheory/Cardinal/Arithmetic.lean

chore(SetTheory/Cardinal/Ordinal): split file (#16990) …

Modified Cardinal.noMaxOrder View on Github →

2024-08-27 18:38

Mathlib/SetTheory/Cardinal/Ordinal.lean

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

Modified Cardinal.noMaxOrder View on Github →

2024-05-21 16:45

Mathlib/SetTheory/Cardinal/Ordinal.lean

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

Added Cardinal.noMaxOrder View on Github →