shadow): Shadow of a set family (#10223)

Commit

4 years ago

feat(combinatorics/set_family/shadow): Shadow of a set family (#10223) This defines `shadow 𝒜` where `𝒜 : finset (finset α))`.

Author

YaelDillies

Parents