Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-07 01:05 655994e2

View on Github →

refactor(data/set/n_ary): extract from data/set/basic (#17836) This is essentially just a copy paste, with one or two whitespace fixes. This split is consistent with how finset/n_ary is its own file, and does a nice job of making data/set/basic a bit shorter. The comment fixes referring to this new file are thanks to #17825.

Estimated changes

deleted theorem set.forall_image2_iff
deleted def set.image2
deleted theorem set.image2_assoc
deleted theorem set.image2_comm
deleted theorem set.image2_congr'
deleted theorem set.image2_congr
deleted theorem set.image2_empty_left
deleted theorem set.image2_empty_right
deleted theorem set.image2_eq_empty_iff
deleted theorem set.image2_image2_left
deleted theorem set.image2_image2_right
deleted theorem set.image2_image_left
deleted theorem set.image2_image_right
deleted theorem set.image2_left
deleted theorem set.image2_left_comm
deleted theorem set.image2_nonempty_iff
deleted theorem set.image2_right
deleted theorem set.image2_right_comm
deleted theorem set.image2_singleton
deleted theorem set.image2_singleton_left
deleted theorem set.image2_subset
deleted theorem set.image2_subset_iff
deleted theorem set.image2_subset_left
deleted theorem set.image2_subset_right
deleted theorem set.image2_swap
deleted theorem set.image2_union_left
deleted theorem set.image2_union_right
deleted def set.image3
deleted theorem set.image3_congr'
deleted theorem set.image3_congr
deleted theorem set.image3_mono
deleted theorem set.image_image2
deleted theorem set.image_image2_distrib
deleted theorem set.mem_image2
deleted theorem set.mem_image2_iff
deleted theorem set.mem_image2_of_mem
deleted theorem set.mem_image3
deleted theorem set.nonempty.image2
added theorem set.forall_image2_iff
added def set.image2
added theorem set.image2_assoc
added theorem set.image2_comm
added theorem set.image2_congr'
added theorem set.image2_congr
added theorem set.image2_empty_left
added theorem set.image2_empty_right
added theorem set.image2_image2_left
added theorem set.image2_image_left
added theorem set.image2_image_right
added theorem set.image2_left
added theorem set.image2_left_comm
added theorem set.image2_right
added theorem set.image2_right_comm
added theorem set.image2_singleton
added theorem set.image2_subset
added theorem set.image2_subset_iff
added theorem set.image2_subset_left
added theorem set.image2_swap
added theorem set.image2_union_left
added theorem set.image2_union_right
added def set.image3
added theorem set.image3_congr'
added theorem set.image3_congr
added theorem set.image3_mono
added theorem set.image_image2
added theorem set.mem_image2
added theorem set.mem_image2_iff
added theorem set.mem_image2_of_mem
added theorem set.mem_image3
added theorem set.nonempty.image2