Commit 2025-03-14 08:06 f59312e8

View on Github →

feat: preimage of a product by restrict (#22558) The preimage of a product of sets by a restriction is the product of the same sets extended with Set.univ outside of the restriction.

Estimated changes

Modified Mathlib/Data/Finset/Pi.lean

modified theorem Finset.piCongrLeft_comp_restrict

added theorem Finset.restrict_preimage

modified def Finset.restrict₂

modified theorem Finset.restrict₂_comp_restrict

modified theorem Finset.restrict₂_comp_restrict₂

modified theorem Finset.restrict₂_def

added theorem Finset.restrict₂_preimage

modified theorem Set.piCongrLeft_comp_restrict