Commit 2021-11-04 17:11 52cd4453

refactor(data/set/pairwise): Indexed sets as arguments to set.pairwise_disjoint (#9898) This will allow to express the bind operation: you can't currently express that the pairwise disjoint union of pairwise disjoint sets pairwise disjoint. Here's the corresponding statement with finset.sup_indep (defined in #9867):

lemma sup_indep.sup {s : finset ι'} {g : ι' → finset ι} {f : ι → α}
  (hs : s.sup_indep (λ i, (g i).sup f)) (hg : ∀ i' ∈ s, (g i').sup_indep f) :
  (s.sup g).sup_indep f :=

You currently can't do set.pairwise_disjoint s (λ i, ⋃ x ∈ g i, f x).