THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines shadows of a set family. The shadow of a set family is the set family of sets we
get by removing any element from any set of the original family. If one pictures
finset α as a big
hypercube (each dimension being membership of a given element), then taking the shadow corresponds
to projecting each finset down once in all available directions.
Main definitions #
finset.shadow: The shadow of a set family. Everything we can get by removing a new element from some set.
finset.up_shadow: The upper shadow of a set family. Everything we can get by adding an element to some set.
We define notation in locale
∂ 𝒜: Shadow of
∂⁺ 𝒜: Upper shadow of
We also maintain the convention that
a, b : α are elements of the ground type,
s, t : finset α
are finsets, and
𝒜, ℬ : finset (finset α) are finset families.
shadow, set family
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
elements from any set in
The shadow of the empty set is empty.
The shadow is monotone.
t is in the shadow of
𝒜 iff we can add an element to it so that the resulting finset is in
The upper shadow of a set family
𝒜 is all sets we can get by adding one element to any set in
𝒜, and the (
k times) iterated upper shadow (
up_shadow^[k]) is all sets we can get by adding
k elements from any set in
- 𝒜.up_shadow = 𝒜.sup (λ (s : finset α), finset.image (λ (a : α), has_insert.insert a s) sᶜ)
The upper shadow of the empty set is empty.
The upper shadow is monotone.
s is in the upper shadow of
𝒜 iff there is an
t ∈ 𝒜 from which we can remove one element
t ∈ ∂^k 𝒜 iff
t is exactly
k elements more than something in