Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-25 22:36 23ffd4ac

View on Github →

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.

Estimated changes