Relations holding pairwise #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
In this file we prove many facts about
pairwise and the set lattice.
If the suprema of columns are pairwise disjoint and suprema of rows as well, then everything is
pairwise disjoint. Not to be confused with
Equivalence between a disjoint bounded union and a dependent sum.