Theorem Ordinal.type_toType

Modification history

2024-12-02 16:40
Mathlib/SetTheory/Ordinal/Basic.lean
feat(SetTheory/Ordinal/Basic): notation `typeLT α = type (α := α) (· < ·)` (#18235)
Modified Ordinal.type_toTypeView on Github →
2024-10-22 17:17
Mathlib/SetTheory/Ordinal/Basic.lean
refactor(SetTheory/Ordinal/Basic): `type_lt` → `type_toType` (#18049) …
Added Ordinal.type_toTypeView on Github →