Commit 2023-07-01 12:39 8a45f5b3

View on Github →

fix: precedence of shadow (#5620)

Estimated changes

Modified Mathlib/Combinatorics/SetFamily/Compression/UV.lean

Modified Mathlib/Combinatorics/SetFamily/LYM.lean

modified theorem Finset.slice_union_shadow_falling_succ

Modified Mathlib/Combinatorics/SetFamily/Shadow.lean

modified theorem Finset.erase_mem_shadow

modified theorem Finset.exists_subset_of_mem_shadow

modified theorem Finset.exists_subset_of_mem_upShadow

modified theorem Finset.insert_mem_upShadow

modified theorem Finset.mem_shadow_iff

modified theorem Finset.mem_shadow_iff_insert_mem

modified theorem Finset.mem_upShadow_iff

modified theorem Finset.mem_upShadow_iff_erase_mem

modified theorem Finset.shadow_empty

modified theorem Finset.shadow_image_compl

modified theorem Finset.shadow_singleton_empty

modified theorem Finset.upShadow_empty

modified theorem Finset.upShadow_image_compl