Commit 2022-09-23 11:55 24b50bfc

View on Github →

chore(data/finset/basic): move disjoint proofs earlier (#16436) This avoids repeating work for disj_union, and takes the stance that disjoint is part of the lattice API.

Estimated changes

Modified src/data/finset/basic.lean

modified theorem disjoint.of_image_finset

modified theorem finset.bot_eq_empty

modified theorem finset.disjoint_bUnion_left

modified theorem finset.disjoint_bUnion_right

modified theorem finset.disjoint_filter

modified theorem finset.disjoint_filter_filter

modified theorem finset.disjoint_image

modified theorem finset.disjoint_map