Theorem Finset.apply_sup_le_sum

Modification history

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_sup_le_sumView on Github →