Shadows #
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.
Notation #
We define notation in locale FinsetFamily
:
∂ 𝒜∂ 𝒜
: 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.
References #
- https://github.com/b-mehta/maths-notes/blob/master/iii/mich/combinatorics.pdf
- http://discretemath.imp.fu-berlin.de/DMII-2015-16/kruskal.pdf
Tags #
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 k
elements from any set in 𝒜
.
Equations
- Finset.shadow 𝒜 = Finset.sup 𝒜 fun s => Finset.image (Finset.erase s) s
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 𝒜
.
Equations
- FinsetFamily.«term∂» = Lean.ParserDescr.node `FinsetFamily.term∂ 90 (Lean.ParserDescr.symbol "∂ ")
The shadow of the empty set is empty.
The shadow is monotone.
s
is in the shadow of 𝒜
iff there is an t ∈ 𝒜∈ 𝒜
from which we can remove one element to
get s
.
t
is in the shadow of 𝒜
iff we can add an element to it so that the resulting finset is in
𝒜
.
The shadow of a family of r
-sets is a family of r - 1
-sets.
s ∈ ∂ 𝒜∈ ∂ 𝒜∂ 𝒜
iff s
is exactly one element less than something from 𝒜
Being in the shadow of 𝒜
means we have a superset in 𝒜
.
t ∈ ∂^k 𝒜∈ ∂^k 𝒜∂^k 𝒜
iff t
is exactly k
elements less than something 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 𝒜
.
Equations
- Finset.upShadow 𝒜 = Finset.sup 𝒜 fun s => Finset.image (fun a => insert a s) (sᶜ)
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 𝒜
.
Equations
- FinsetFamily.«term∂⁺» = Lean.ParserDescr.node `FinsetFamily.term∂⁺ 90 (Lean.ParserDescr.symbol "∂⁺ ")
The upper shadow of the empty set is empty.
The upper shadow is monotone.
The upper shadow of a family of r
-sets is a family of r + 1
-sets.
t
is in the upper shadow of 𝒜
iff we can remove an element from it so that the resulting
finset is in 𝒜
.
s ∈ ∂⁺ 𝒜∈ ∂⁺ 𝒜∂⁺ 𝒜⁺ 𝒜
iff s
is exactly one element less than something from 𝒜
.
Being in the upper shadow of 𝒜
means we have a superset in 𝒜
.
t ∈ ∂^k 𝒜∈ ∂^k 𝒜∂^k 𝒜
iff t
is exactly k
elements more than something in 𝒜
.