Commit 2025-09-30 11:00 49fa7a73

View on Github →

feat(Finset/Interval): improve computation performance (#30078) Use map on (t \ s).powerset instead of filtering t.powerset.

Estimated changes

Modified Mathlib/Data/Finset/Disjoint.lean

added theorem Finset.disjUnion_inj_left

added theorem Finset.disjUnion_inj_right

Modified Mathlib/Data/Finset/Interval.lean

modified theorem Finset.Icc_eq_filter_powerset

modified theorem Finset.Ico_eq_filter_ssubsets

modified theorem Finset.Iic_eq_powerset

modified theorem Finset.Iio_eq_ssubsets

modified theorem Finset.Ioc_eq_filter_powerset

modified theorem Finset.Ioo_eq_filter_ssubsets