Commit 2023-03-19 19:21 19a349d6

View on Github →

feat: Set.image2_image2_image2_comm (#2992) Match https://github.com/leanprover-community/mathlib/pull/18172

Estimated changes

Modified Mathlib/Data/Finset/NAry.lean

modified theorem Finset.image_subset_image₂_left

modified theorem Finset.image_subset_image₂_right

added theorem Finset.image₂_image₂_image₂_comm

Modified Mathlib/Data/Set/NAry.lean

added theorem Set.image2_image2_image2_comm