Theorem Finset.Finset.filter_mem_eq_of_subset

Modification history

2026-05-10 13:51
Mathlib/Data/Finset/Filter.lean
feat: the cardinal of a finset is an ite sum over a bigger finset (#37831) …
Added Finset.Finset.filter_mem_eq_of_subsetView on Github →