Commit 2022-05-13 05:13 644cae5e

feat(set_theory/cardinal/cofinality): Move fundamental sequence results to namespace (#14020) We put most results about fundamental sequences in the is_fundamental_sequence namespace. We also take the opportunity to add a simple missing theorem, ord_cof.