Commit 2022-12-14 16:48 a5d78c33

View on Github →

feat: port Data.Set.Prod (#1004) fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e

depends on: #1000

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Set/Prod.lean

added theorem Antitone.set_prod

added theorem AntitoneOn.set_prod

added theorem Monotone.set_prod

added theorem MonotoneOn.set_prod

added theorem Set.Nonempty.fst

added theorem Set.Nonempty.prod

added theorem Set.Nonempty.snd

added theorem Set.diag_preimage_prod

added theorem Set.diag_preimage_prod_self

added def Set.diagonal

added theorem Set.disjoint_diagonal_offDiag

added theorem Set.disjoint_prod

added theorem Set.disjoint_univ_pi

added theorem Set.empty_pi

added theorem Set.empty_prod

added theorem Set.eval_image_pi

added theorem Set.eval_image_pi_subset

added theorem Set.eval_image_univ_pi

added theorem Set.eval_image_univ_pi_subset

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.fst_image_prod_subset

added theorem Set.image2_curry

added theorem Set.image2_mk_eq_prod

added theorem Set.image_prod

added theorem Set.image_prod_mk_subset_prod

added theorem Set.image_prod_mk_subset_prod_left

added theorem Set.image_prod_mk_subset_prod_right

added theorem Set.image_swap_prod

added theorem Set.image_uncurry_prod

added theorem Set.insert_pi

added theorem Set.insert_prod

added theorem Set.inter_prod

added theorem Set.mem_diagonal

added theorem Set.mem_diagonal_iff

added theorem Set.mem_offDiag

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.mk_preimage_prod_left

added theorem Set.mk_preimage_prod_left_eq_empty

added theorem Set.mk_preimage_prod_left_eq_if

added theorem Set.mk_preimage_prod_left_fn_eq_if

added theorem Set.mk_preimage_prod_right

added theorem Set.mk_preimage_prod_right_eq_empty

added theorem Set.mk_preimage_prod_right_eq_if

added theorem Set.mk_preimage_prod_right_fn_eq_if

added def Set.offDiag

added theorem Set.offDiag_empty

added theorem Set.offDiag_eq_empty

added theorem Set.offDiag_eq_sep_prod

added theorem Set.offDiag_insert

added theorem Set.offDiag_inter

added theorem Set.offDiag_mono

added theorem Set.offDiag_nonempty

added theorem Set.offDiag_singleton

added theorem Set.offDiag_subset_prod

added theorem Set.offDiag_union

added theorem Set.offDiag_univ

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_subset_pi_iff

added theorem Set.pi_univ

added theorem Set.pi_update_of_mem

added theorem Set.pi_update_of_not_mem

added theorem Set.preimage_coe_coe_diagonal

added theorem Set.preimage_pi

added theorem Set.preimage_prod_map_prod

added theorem Set.preimage_swap_prod

added def Set.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_eq_iff_eq

added theorem Set.prod_eq_prod_iff

added theorem Set.prod_eq_prod_iff_of_nonempty

added theorem Set.prod_image_image_eq

added theorem Set.prod_insert

added theorem Set.prod_inter

added theorem Set.prod_inter_prod

added theorem Set.prod_mk_mem_set_prod_eq

added theorem Set.prod_mono

added theorem Set.prod_mono_left

added theorem Set.prod_mono_right

added theorem Set.prod_nonempty_iff

added theorem Set.prod_preimage_eq

added theorem Set.prod_preimage_left

added theorem Set.prod_preimage_right

added theorem Set.prod_range_range_eq

added theorem Set.prod_range_univ_eq

added theorem Set.prod_sdiff_diagonal

added theorem Set.prod_self_ssubset_prod_self

added theorem Set.prod_self_subset_prod_self

added theorem Set.prod_singleton

added theorem Set.prod_sub_preimage_iff

added theorem Set.prod_subset_compl_diagonal_iff_disjoint

added theorem Set.prod_subset_iff

added theorem Set.prod_subset_preimage_fst

added theorem Set.prod_subset_preimage_snd

added theorem Set.prod_subset_prod_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_diag

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.singleton_prod_singleton

added theorem Set.snd_image_prod

added theorem Set.snd_image_prod_subset

added theorem Set.subset_eval_image_pi

added theorem Set.subset_pi_eval_image

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_eq_empty_iff

added theorem Set.univ_pi_ite

added theorem Set.univ_pi_nonempty_iff

added theorem Set.univ_pi_singleton

added theorem Set.univ_pi_subset_univ_pi_iff

added theorem Set.univ_pi_update

added theorem Set.univ_pi_update_univ

added theorem Set.univ_prod

added theorem Set.univ_prod_univ

added theorem Set.update_preimage_pi

added theorem Set.update_preimage_univ_pi