Commit 2025-01-20 15:19 914ded28

View on Github →

feat: the pairs {t, insert a t} are pairwise disjoint (#20062) This will be used to prove the existence of symmetric chain decompositions. From LeanCamCombi

Estimated changes

Modified Mathlib/Data/Finset/Basic.lean

added theorem Finset.pairwiseDisjoint_iff

Modified Mathlib/Data/Finset/Defs.lean

Modified Mathlib/Data/Finset/Powerset.lean

added theorem Finset.pairwiseDisjoint_pair_insert

Modified Mathlib/Data/Set/Basic.lean

added theorem Set.insert_diff_self_of_mem

added theorem Set.insert_erase_invOn

Modified Mathlib/Data/Set/Pairwise/Lattice.lean

added theorem Set.pairwiseDisjoint_iff

added theorem Set.pairwiseDisjoint_pair_insert