Commit 2021-12-23 16:33 2be37b00

View on Github →

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.

Estimated changes

Modified src/combinatorics/set_family/shadow.lean

added theorem finset.exists_subset_of_mem_up_shadow

added theorem finset.insert_mem_up_shadow

added theorem finset.mem_up_shadow_iff

added theorem finset.mem_up_shadow_iff_erase_mem

added theorem finset.mem_up_shadow_iff_exists_mem_card_add

added theorem finset.mem_up_shadow_iff_exists_mem_card_add_one

added theorem finset.shadow_image_compl

added def finset.up_shadow

added theorem finset.up_shadow_empty

added theorem finset.up_shadow_image_compl

added theorem finset.up_shadow_monotone