Mathlib v3 is deprecated. Go to Mathlib v4

Theorem cardinal.mk_ordinal_out

Modification history

2022-06-05 07:36
src/set_theory/ordinal/basic.lean
refactor(set_theory/*): change `omega` to `aleph_0` + golf (#14467) …
Modified cardinal.mk_ordinal_outView on Github →
2022-03-29 05:57
src/set_theory/cardinal_ordinal.lean
feat(set_theory/{ordinal_arithmetic, game/nim}): Minimum excluded ordinal (#12659) …
Modified cardinal.mk_ordinal_outView on Github →
2022-03-04 17:34
src/set_theory/cardinal_ordinal.lean
feat(set_theory/cofinality): `cof_eq_Inf_lsub` (#12314) …
Added cardinal.mk_ordinal_outView on Github →