Commit 2022-12-23 16:03 d90ae095

View on Github →

chore: move basic lemmas to basic files (#1109) synchronize with https://github.com/leanprover-community/mathlib/pull/17882 Make disjoint_singleton @[simp 1100] because the linter complains it is not in simpNF (because of disjoint_singleton_left and disjoint_singleton_right). Removing simp of disjoint_singleton, making disjoint_singleton_left have a greater priority than disjoint_singleton_right, then disjoint_singleton can be proved by simp.

Estimated changes

added theorem Antitone.inter
added theorem Antitone.union
added theorem AntitoneOn.inter
added theorem AntitoneOn.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 MonotoneOn.inter
added theorem MonotoneOn.union
added theorem Set.antitone_bforall
added theorem Set.antitone_setOf
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_setOf
added theorem Set.not_disjoint_iff
added theorem Set.subset_diff
added theorem Set.univ_disjoint
added theorem Disjoint.image
added theorem Set.InjOn.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 AntitoneOn.inter
deleted theorem AntitoneOn.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 MonotoneOn.inter
deleted theorem MonotoneOn.union
deleted theorem Set.InjOn.image_inter
deleted theorem Set.antitone_bforall
deleted theorem Set.antitone_setOf
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.monotone_image
deleted theorem Set.monotone_setOf
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