Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-07-16 14:06 20fca1ce

View on Github →

feat(data/finset): disjoint finsets

Estimated changes

Modified data/finset.lean

added theorem finset.card_disjoint_union

added theorem finset.disjoint_empty_left

added theorem finset.disjoint_empty_right

added theorem finset.disjoint_iff_inter_eq_empty

added theorem finset.disjoint_iff_ne

added theorem finset.disjoint_insert_left

added theorem finset.disjoint_insert_right

added theorem finset.disjoint_left

added theorem finset.disjoint_of_subset_left

added theorem finset.disjoint_of_subset_right

added theorem finset.disjoint_right

added theorem finset.disjoint_singleton

added theorem finset.disjoint_union_left

added theorem finset.disjoint_union_right

deleted theorem finset.inter_eq_empty_iff_disjoint

added theorem finset.singleton_disjoint

Modified data/set/lattice.lean

added theorem disjoint_comm