Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-20 05:38 0cf8a98b

View on Github →

chore(data/set): a few more lemmas about image2 (#4695) Also add @[simp] to set.image2_singleton_left and set.image2_singleton_rigt.

Estimated changes

added theorem set.exists_prod_set
added theorem set.forall_image2_iff
added theorem set.image2_assoc
modified theorem set.image2_singleton
modified theorem set.image2_singleton_left
modified theorem set.image2_singleton_right
added theorem set.image2_subset_iff