feat(set_theory/cofinality): Every ordinal has a fundamental sequence (#12317)
feat(set_theory/cofinality): Every ordinal has a fundamental sequence (#12317)





leanprover-community/mathlib,leanprover-community/mathlib