Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-13 09:36 9d73418c

View on Github →

split(data/set/prod): split off data.set.basic (#10739) This moves set.prod, set.pi and set.diagonal from data.set.basic to a new file data.set.prod. I'm crediting

  • Mario for set.prod from bd013e8089378e8057dc7e93c9eaf2c8ebaf25a2
  • Johannes for set.pi from da7bbd7fc2c80a785f7992bb7751304f6cafe235
  • Patrick for set.diagonal from #3118

Estimated changes

deleted def set.diagonal
deleted theorem set.diagonal_eq_range
deleted theorem set.empty_pi
deleted theorem set.empty_prod
deleted theorem set.eval_image_pi
deleted theorem set.eval_image_univ_pi
deleted theorem set.eval_preimage'
deleted theorem set.eval_preimage
deleted theorem set.exists_prod_set
deleted theorem set.forall_prod_set
deleted theorem set.fst_image_prod
deleted theorem set.fst_image_prod_subset
deleted theorem set.image_prod
deleted theorem set.image_swap_prod
deleted theorem set.insert_pi
deleted theorem set.insert_prod
deleted theorem set.mem_diagonal
deleted theorem set.mem_pi
deleted theorem set.mem_prod
deleted theorem set.mem_prod_eq
deleted theorem set.mem_univ_pi
deleted theorem set.mk_mem_prod
deleted theorem set.mk_preimage_prod
deleted theorem set.mk_preimage_prod_left
deleted theorem set.nonempty.fst
deleted theorem set.nonempty.prod
deleted theorem set.nonempty.snd
deleted def set.pi
deleted theorem set.pi_congr
deleted theorem set.pi_eq_empty
deleted theorem set.pi_eq_empty_iff
deleted theorem set.pi_if
deleted theorem set.pi_inter_compl
deleted theorem set.pi_inter_distrib
deleted theorem set.pi_mono
deleted theorem set.pi_nonempty_iff
deleted theorem set.pi_univ
deleted theorem set.pi_update_of_mem
deleted theorem set.pi_update_of_not_mem
deleted theorem set.preimage_swap_prod
deleted theorem set.prod_diff_prod
deleted theorem set.prod_empty
deleted theorem set.prod_eq
deleted theorem set.prod_eq_empty_iff
deleted theorem set.prod_image_image_eq
deleted theorem set.prod_insert
deleted theorem set.prod_inter_prod
deleted theorem set.prod_mono
deleted theorem set.prod_nonempty_iff
deleted theorem set.prod_preimage_eq
deleted theorem set.prod_preimage_left
deleted theorem set.prod_preimage_right
deleted theorem set.prod_range_range_eq
deleted theorem set.prod_range_univ_eq
deleted theorem set.prod_singleton
deleted theorem set.prod_sub_preimage_iff
deleted theorem set.prod_subset_iff
deleted theorem set.prod_subset_prod_iff
deleted theorem set.prod_union
deleted theorem set.prod_univ
deleted theorem set.prod_univ_range_eq
deleted theorem set.range_dcomp
deleted theorem set.range_pair_subset
deleted theorem set.range_prod_map
deleted theorem set.singleton_pi'
deleted theorem set.singleton_pi
deleted theorem set.singleton_prod
deleted theorem set.snd_image_prod
deleted theorem set.snd_image_prod_subset
deleted theorem set.subset_pi_eval_image
deleted theorem set.union_pi
deleted theorem set.union_prod
deleted theorem set.univ_pi_empty
deleted theorem set.univ_pi_eq_empty
deleted theorem set.univ_pi_eq_empty_iff
deleted theorem set.univ_pi_ite
deleted theorem set.univ_pi_nonempty_iff
deleted theorem set.univ_pi_update
deleted theorem set.univ_pi_update_univ
deleted theorem set.univ_prod
deleted theorem set.univ_prod_univ
deleted theorem set.update_preimage_pi
added def set.diagonal
added theorem set.diagonal_eq_range
added theorem set.empty_pi
added theorem set.empty_prod
added theorem set.eval_image_pi
added theorem set.eval_image_univ_pi
added theorem set.eval_preimage'
added theorem set.eval_preimage
added theorem set.exists_prod_set
added theorem set.forall_prod_set
added theorem set.fst_image_prod
added theorem set.image_prod
added theorem set.image_swap_prod
added theorem set.insert_pi
added theorem set.insert_prod
added theorem set.mem_diagonal
added theorem set.mem_pi
added theorem set.mem_prod
added theorem set.mem_prod_eq
added theorem set.mem_univ_pi
added theorem set.mk_mem_prod
added theorem set.mk_preimage_prod
added theorem set.nonempty.fst
added theorem set.nonempty.prod
added theorem set.nonempty.snd
added def set.pi
added theorem set.pi_congr
added theorem set.pi_eq_empty
added theorem set.pi_eq_empty_iff
added theorem set.pi_if
added theorem set.pi_inter_compl
added theorem set.pi_inter_distrib
added theorem set.pi_mono
added theorem set.pi_nonempty_iff
added theorem set.pi_univ
added theorem set.pi_update_of_mem
added theorem set.preimage_swap_prod
added theorem set.prod_diff_prod
added theorem set.prod_empty
added theorem set.prod_eq
added theorem set.prod_eq_empty_iff
added theorem set.prod_insert
added theorem set.prod_inter_prod
added theorem set.prod_mono
added theorem set.prod_nonempty_iff
added theorem set.prod_preimage_eq
added theorem set.prod_preimage_left
added theorem set.prod_range_univ_eq
added theorem set.prod_singleton
added theorem set.prod_subset_iff
added theorem set.prod_union
added theorem set.prod_univ
added theorem set.prod_univ_range_eq
added theorem set.range_dcomp
added theorem set.range_pair_subset
added theorem set.range_prod_map
added theorem set.singleton_pi'
added theorem set.singleton_pi
added theorem set.singleton_prod
added theorem set.snd_image_prod
added theorem set.union_pi
added theorem set.union_prod
added theorem set.univ_pi_empty
added theorem set.univ_pi_eq_empty
added theorem set.univ_pi_ite
added theorem set.univ_pi_update
added theorem set.univ_prod
added theorem set.univ_prod_univ
added theorem set.update_preimage_pi