Commit 2022-03-04 17:34 fab59cb8

View on Github →

feat(set_theory/cofinality): cof_eq_Inf_lsub (#12314) This much nicer characterization of cofinality will allow us to prove various theorems relating it to lsub and blsub.

Estimated changes

Modified src/set_theory/cardinal_ordinal.lean

added theorem cardinal.mk_ordinal_out

Modified src/set_theory/cofinality.lean

added theorem ordinal.cof_eq_Inf_lsub

added theorem ordinal.cof_lsub_def_nonempty