Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ordinal.type_lt

Modification history

2022-04-21 20:30
src/set_theory/ordinal/basic.lean
chore(set_theory/ordinal/basic): Small style tweaks (#13561)
Modified ordinal.type_ltView on Github →
2022-03-07 10:15
src/set_theory/ordinal.lean
refactor(set_theory/*): `o.out.r` → `<` (#12468) …
Modified ordinal.type_ltView on Github →
2017-12-11 05:07
data/ordinal.lean
feat(data/ordinal): more ordinals
Added ordinal.type_ltView on Github →