mathlib

2be37b00 - feat(combinatorics/set_family/shadow): Upper shadow of a set family (#10956)

feat(combinatorics/set_family/shadow): Upper shadow of a set family (#10956) This defines the upper shadow of `𝒜 : finset (finset α)`, which is the dual of the shadow. Instead of removing each element from each set, we add each element not in each set.