mathlib3
ffa6e6d6 - feat(set_theory/cardinal): `sum_le_sup_lift` (#12513)

Commit

3 years ago

feat(set_theory/cardinal): `sum_le_sup_lift` (#12513) This is a universe-polymorphic version of `sum_le_sup`.

Author

vihdzp

Parents