pairwise): Taking the `bUnion` is injective (#17052)

Commit

3 years ago

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.

Author

YaelDillies

Parents

12a7da10

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

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