Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-21 12:10 0f9edf98

View on Github →

feat(data/set/[basic|prod]): make ×ˢ bind more strongly, and define mem.out (#13422)

  • This means that ×ˢ does not behave the same as ∪ or ∩ around ⁻¹' or '', but I think that is fine.
  • From the sphere eversion project

Estimated changes

added theorem set.has_mem.mem.out
added theorem set.mem_set_of
modified theorem set.mem_set_of_eq
modified theorem set.nmem_set_of_eq
modified theorem set.image_div_prod
modified theorem set.image_mul_prod
modified theorem set.image_smul_prod
modified theorem set.image_vsub_prod
modified theorem set.fst_image_prod
modified theorem set.fst_image_prod_subset
modified theorem set.image_prod
modified theorem set.image_swap_prod
modified theorem set.mk_preimage_prod_left
modified theorem set.mk_preimage_prod_right
modified theorem set.preimage_swap_prod
modified theorem set.prod_eq_empty_iff
modified theorem set.prod_subset_iff
modified theorem set.snd_image_prod
modified theorem set.snd_image_prod_subset
modified theorem equiv.prod_comm_image