Commit 2025-10-23 17:08 0fb521d3

View on Github →

feat(Data/Set/Pairwise): prove pairwise results for Chains, move Set.pairwise_iUnion₂ (#28119) Initiate a new file Data/Set/Pairwise/Chain.lean which makes some Pairwise results available to the IsChain predicate. In the process, move Set.pairwise_iUnion₂ to group it with similar results. Perform some variable harmonization. Part of Carleson, original result by Edward van de Meent. Moves:

Set.pairwise_iUnion₂: from Data.Set.Lattice to Data.Set.Pairwise.Lattice

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Set/Lattice.lean

deleted theorem Set.pairwise_iUnion₂

Created Mathlib/Data/Set/Pairwise/Chain.lean

added theorem IsChain.pairwiseDisjoint_iUnion₂

added theorem IsChain.pairwiseDisjoint_sUnion

added theorem IsChain.pairwise_iUnion₂

added theorem IsChain.pairwise_sUnion

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

modified theorem Set.pairwise_iUnion

added theorem Set.pairwise_iUnion₂

added theorem Set.pairwise_iUnion₂_iff

modified theorem Set.pairwise_sUnion