mathlib

644cae5e - feat(set_theory/cardinal/cofinality): Move fundamental sequence results to namespace (#14020)

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