mathlib

ba9ead03 - feat(order/sup_indep): lemmas about `pairwise` and `set.pairwise` (#12590)

feat(order/sup_indep): lemmas about `pairwise` and `set.pairwise` (#12590) The `disjoint` lemmas can now be stated in terms of these two `pairwise` definitions. This wasn't previously possible as these definitions were not yet imported. This also adds the `iff` versions of these lemmas, and a docstring tying them all together.