Commit 2022-01-24 22:53 12fde093

feat(data/finset/finsupp): Finitely supported product of finsets (#11639) Define

• finsupp.indicator: Similar to finsupp.on_finset except that it only requires a partially defined function. This is more compatible with finset.pi.
• finset.finsupp : finset ι → (ι → finset α) → finset (ι →₀ α): Finitely supported product of finsets.
• finsupp.pi : (ι →₀ finset α) → finset (ι →₀ α): The set of finitely supported functions whose i-th value lies in the i-th of a given finset-valued finsupp.