Theorem Set.pairwise_iUnion₂

Modification history

2025-10-23 17:08
Mathlib/Data/Set/Lattice.lean
feat(Data/Set/Pairwise): prove pairwise results for Chains, move `Set.pairwise_iUnion₂` (#28119) …
Modified Set.pairwise_iUnion₂View on Github →
2025-03-28 23:10
Mathlib/Data/Set/Lattice.lean
feat(Data/Set/Lattice): add `pairwise_iUnion₂` (#23416) …
Added Set.pairwise_iUnion₂View on Github →