Commit 2022-12-15 12:53 cbae1b5e

View on Github →

chore: set.image lemmas (#1045) Match https://github.com/leanprover-community/mathlib/pull/17924, https://github.com/leanprover-community/mathlib/pull/17945

Estimated changes

Modified Mathlib/Data/Set/Image.lean

modified theorem Set.image_inter

Modified Mathlib/Data/Set/NAry.lean

added theorem Set.image2_curry

added theorem Set.image2_inter_left

added theorem Set.image2_inter_right

added theorem Set.image2_mk_eq_prod

added theorem Set.image_prod

added theorem Set.image_uncurry_prod

Modified Mathlib/Data/Set/Prod.lean

deleted theorem Set.image2_curry

deleted theorem Set.image2_mk_eq_prod

deleted theorem Set.image_prod

deleted theorem Set.image_uncurry_prod