chore(set_theory/cardinal): `min` → `Inf` (#12517)
chore(set_theory/cardinal): `min` → `Inf` (#12517)

Various definitions are awkwardly stated in terms of minima of subtypes. We instead rewrite them as infima and golf them. Further, we protect `cardinal.min` to avoid confusion with `linear_order.min`.





leanprover-community/mathlib,leanprover-community/mathlib