mathlib

ba22440f - feat(set_theory/cardinal/cofinality): use `bounded` and `unbounded` (#14438)

feat(set_theory/cardinal/cofinality): use `bounded` and `unbounded` (#14438) We change `∀ a, ∃ b ∈ s, ¬ r b a` to its def-eq predicate `unbounded r s`, and similarly for `bounded r s`.