Commit 2022-03-09 09:05 55d1f3e8

View on Github →

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.

Estimated changes

Modified src/set_theory/cardinal.lean

modified theorem cardinal.le_min

modified theorem cardinal.le_sup

modified theorem cardinal.lift_min

deleted def cardinal.min

modified theorem cardinal.min_eq

modified theorem cardinal.min_le

added theorem cardinal.nonempty_sup

added theorem cardinal.succ_nonempty

modified def cardinal.sup