Commit 2021-11-11 19:35 9a30dcfd

View on Github →

feat(data/finset/pairwise): Interaction of set.pairwise_disjoint with finset (#10244) This proves a few results about set.pairwise_disjoint and finset that couldn't go data.set.pairwise because of cyclic imports.

Estimated changes

Created src/data/finset/pairwise.lean

added theorem finset.pairwise_disjoint_range_singleton

added theorem set.pairwise_disjoint.bUnion_finset

added theorem set.pairwise_disjoint.elim_finset

added theorem set.pairwise_disjoint.image_finset_of_le

Modified src/data/set/pairwise.lean

added theorem set.pairwise_disjoint.bUnion