mathlib

fab59cb8 - feat(set_theory/cofinality): `cof_eq_Inf_lsub` (#12314)

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`.