Theorem Finset.Finset.disjoint_filter_and_not_filter

Modification history

2024-12-05 16:41
Mathlib/Data/Finset/Filter.lean
feat(Algebra/BigOperators/Group/Finset) : Finset.prod_disjoint_filters (#19712) …
Added Finset.Finset.disjoint_filter_and_not_filterView on Github →