Theorem Finset.apply_union_le_sum

Modification history

2026-02-21 12:00
Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
chore: weaken `PartialOrder` to `Preorder` in `IsOrderedMonoid` hypothesis (#34295) …
Modified Finset.apply_union_le_sumView on Github →
2025-10-09 08:14
Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
chore(Algebra/Order/BigOperators/Group/{Finset, Multiset}): generalize results to `(Mul)(Add)LeftMono` (#29864) …
Modified Finset.apply_union_le_sumView on Github →
2025-08-22 15:25
Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
feat(Data/Set/Card): add lemmas of the form `card_Union_le` (#28534) …
Added Finset.apply_union_le_sumView on Github →