Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-21 14:13 3d954923

View on Github →

chore(data/set/lattice): move basic lemmas to basic files (#17882) This PR moves some lemmas in data.set.lattice to data.set.basic, data.set.image, and data.set.function. They are basic enough and do not depend on the set lattice. This also helps #17880 to split data.set.pairwise and reduce the dependency of many files. mathlib4 PR: https://github.com/leanprover-community/mathlib4/pull/1109

Estimated changes

added theorem antitone.inter
added theorem antitone.union
added theorem antitone_on.inter
added theorem antitone_on.union
added theorem disjoint.inter_left'
added theorem disjoint.inter_left
added theorem disjoint.inter_right'
added theorem disjoint.inter_right
added theorem disjoint.ne_of_mem
added theorem disjoint.union_left
added theorem disjoint.union_right
added theorem monotone.inter
added theorem monotone.union
added theorem monotone_on.inter
added theorem monotone_on.union
added theorem set.antitone_bforall
added theorem set.antitone_set_of
added theorem set.disjoint_diff
added theorem set.disjoint_empty
added theorem set.disjoint_of_subset
added theorem set.disjoint_singleton
added theorem set.disjoint_univ
added theorem set.empty_disjoint
added theorem set.monotone_set_of
added theorem set.not_disjoint_iff
added theorem set.subset_diff
added theorem set.univ_disjoint
added theorem disjoint.image
added theorem set.inj_on.image_inter
added theorem disjoint.of_image
added theorem disjoint.of_preimage
added theorem disjoint.preimage
added theorem set.disjoint_image_iff
added theorem set.monotone_image
added theorem set.preimage_eq_empty
deleted theorem antitone.inter
deleted theorem antitone.union
deleted theorem antitone_on.inter
deleted theorem antitone_on.union
deleted theorem disjoint.image
deleted theorem disjoint.inter_left'
deleted theorem disjoint.inter_left
deleted theorem disjoint.inter_right'
deleted theorem disjoint.inter_right
deleted theorem disjoint.ne_of_mem
deleted theorem disjoint.of_image
deleted theorem disjoint.of_preimage
deleted theorem disjoint.preimage
deleted theorem disjoint.union_left
deleted theorem disjoint.union_right
deleted theorem monotone.inter
deleted theorem monotone.union
deleted theorem monotone_on.inter
deleted theorem monotone_on.union
deleted theorem set.antitone_bforall
deleted theorem set.antitone_set_of
deleted theorem set.disjoint_diff
deleted theorem set.disjoint_empty
deleted theorem set.disjoint_image_iff
deleted theorem set.disjoint_image_image
deleted theorem set.disjoint_of_subset
deleted theorem set.disjoint_preimage_iff
deleted theorem set.disjoint_singleton
deleted theorem set.disjoint_union_left
deleted theorem set.disjoint_union_right
deleted theorem set.disjoint_univ
deleted theorem set.empty_disjoint
deleted theorem set.inj_on.image_inter
deleted theorem set.monotone_image
deleted theorem set.monotone_set_of
deleted theorem set.not_disjoint_iff
deleted theorem set.preimage_eq_empty
deleted theorem set.preimage_eq_empty_iff
deleted theorem set.subset_diff
deleted theorem set.univ_disjoint