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.





leanprover-community/mathlib,leanprover-community/mathlib