mathlib

70d5733d - feat(combinatorics/set_family/compression/down): Down-compression (#15246)

feat(combinatorics/set_family/compression/down): Down-compression (#15246) Define the down-compression of set families. Down-compressing `𝒜 : finset (finset α)` along `a : α` means removing `a` for the elements of `𝒜` that contain it for the sets whose image is not yet there. Move `finset.member_subfamily`/`finset.non_member_subfamily` to that new file and rename them to `finset.member_section`/`finset.non_member_section` to match the literature.