Commit 2023-01-17 13:16 98c12958

View on Github →

feat: port Data.Finset.Pairwise (#1624)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Finset/Pairwise.lean

added theorem Finset.pairwiseDisjoint_range_singleton

added theorem List.pairwiseDisjoint_iff_coe_toFinset_pairwise_disjoint

added theorem List.pairwise_disjoint_of_coe_toFinset_pairwiseDisjoint

added theorem List.pairwise_iff_coe_toFinset_pairwise

added theorem List.pairwise_of_coe_toFinset_pairwise

added theorem Set.PairwiseDisjoint.bunionᵢ_finset

added theorem Set.PairwiseDisjoint.elim_finset

added theorem Set.PairwiseDisjoint.image_finset_of_le