Theorems · Definition · combinatorics
Finset.shadow
{α : Type u_1} → [DecidableEq α] → Finset (Finset α) → Finset (Finset α)The shadow of a set family 𝒜 is all sets we can get by removing one element from any set in
𝒜, and the (k times) iterated shadow (shadow^[k]) is all sets we can get by removing k
elements from any set in 𝒜.
- Defined in
- Mathlib.Combinatorics.SetFamily.Shadow
- Cited by
- 35 results in Mathlib
- Foundations
- Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DecidableEq
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement and proof · cited by 13,712
- Finset.imageproof · cited by 910
- Finset.supproof · cited by 530
- Finset.eraseproof · cited by 455
Cited by35
Results whose statement or proof uses this declaration.
- Finset.mem_shadow_iffstatement · cited by 3
- Set.Sized.shadowstatement and proof · cited by 3
- Finset.shadow_monotonestatement · cited by 2
- Finset.mem_shadow_iterate_iff_exists_sdiffstatement · cited by 2
- Finset.erase_mem_shadowstatement · cited by 2
- Finset.local_lubell_yamamoto_meshalkin_inequality_divstatement and proof · cited by 2
- Finset.local_lubell_yamamoto_meshalkin_inequality_mulstatement and proof · cited by 2
- Finset.shadow_monostatement · cited by 1
- Finset.iterated_kkstatement and proof · cited by 1
- Finset.kruskal_katonastatement and proof · cited by 1
- Finset.kruskal_katona_lovasz_formstatement and proof · cited by 1
- Finset.shadow_singleton_emptystatement · cited by 1