Commit 2020-09-26 07:58 c2f896fe

View on Github →

feat(data/set): add some lemmas (#4263) Some lemmas about sets, mostly involving disjointness I also sneaked in the lemma (λ x : α, y) = const α y which is useful to rewrite with.

Estimated changes

Modified src/data/set/basic.lean

added theorem set.preimage_swap_prod

Modified src/data/set/lattice.lean

added theorem disjoint.preimage

added theorem disjoint.union_left

added theorem disjoint.union_right

deleted theorem set.disjoint.preimage

deleted theorem set.disjoint.union_left

deleted theorem set.disjoint.union_right

modified theorem set.disjoint_iff_inter_eq_empty

modified theorem set.disjoint_left

modified theorem set.disjoint_of_subset_left

modified theorem set.disjoint_of_subset_right

modified theorem set.disjoint_right

modified theorem set.disjoint_singleton_left

modified theorem set.disjoint_singleton_right

modified theorem set.disjoint_union_left

modified theorem set.disjoint_union_right

added theorem set.disjoint_univ

modified theorem set.not_disjoint_iff

added theorem set.preimage_eq_empty

added theorem set.preimage_eq_empty_iff

added theorem set.univ_disjoint

Modified src/logic/function/basic.lean

added theorem function.const_def