Commit 2023-01-30 06:57 d389d10b

View on Github →

feat: port Combinatorics.SetFamily.Shadow (#1938)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/SetFamily/Shadow.lean

added theorem Finset.erase_mem_shadow

added theorem Finset.exists_subset_of_mem_shadow

added theorem Finset.exists_subset_of_mem_upShadow

added theorem Finset.insert_mem_upShadow

added theorem Finset.mem_shadow_iff

added theorem Finset.mem_shadow_iff_exists_mem_card_add

added theorem Finset.mem_shadow_iff_exists_mem_card_add_one

added theorem Finset.mem_shadow_iff_insert_mem

added theorem Finset.mem_upShadow_iff

added theorem Finset.mem_upShadow_iff_erase_mem

added theorem Finset.mem_upShadow_iff_exists_mem_card_add

added theorem Finset.mem_upShadow_iff_exists_mem_card_add_one

added def Finset.shadow

added theorem Finset.shadow_empty

added theorem Finset.shadow_image_compl

added theorem Finset.shadow_monotone

added theorem Finset.shadow_singleton_empty

added theorem Finset.sized_shadow_iff

added def Finset.upShadow

added theorem Finset.upShadow_empty

added theorem Finset.upShadow_image_compl

added theorem Finset.upShadow_monotone