feat(data/set/pairwise): Taking the `bUnion` is injective (#17052)
feat(data/set/pairwise): Taking the `bUnion` is injective (#17052)

... in the set bounding the union, when all sets in the family are pairwise disjoint and nonempty.





leanprover-community/mathlib,leanprover-community/mathlib