Commit 2025-08-22 15:25 14af3231

View on Github →

feat(Data/Set/Card): add lemmas of the form card_Union_le (#28534) Add Finset/Fintype/Finite and ncard/encard variants. Zulip thread

Estimated changes

Modified Mathlib/Algebra/Order/BigOperators/Group/Finset.lean

added theorem Finset.apply_sup_le_sum

added theorem Finset.apply_union_le_sum

Modified Mathlib/Data/Set/Card/Arithmetic.lean

added theorem Finset.set_encard_biUnion_le

added theorem Finset.set_ncard_biUnion_le

added theorem Set.Finite.encard_biUnion_le

added theorem Set.Finite.ncard_biUnion_le

added theorem Set.encard_iUnion_le_of_finite

added theorem Set.encard_iUnion_le_of_fintype

added theorem Set.ncard_iUnion_le_of_finite

added theorem Set.ncard_iUnion_le_of_fintype