# 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 `𝒜`

.

## Instances For

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 `𝒜`

.

## Instances For

The shadow of the empty set is empty.

The shadow is monotone.

`s`

is in the shadow of `𝒜`

iff there is a `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 𝒜`

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 (`upShadow^[k]`

) is all sets we can get by adding
`k`

elements from any set in `𝒜`

.

## Instances For

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 (`upShadow^[k]`

) is all sets we can get by adding
`k`

elements from any set in `𝒜`

.

## Instances For

The upper shadow of the empty set is empty.

The upper shadow is monotone.

`s`

is in the upper shadow of `𝒜`

iff there is a `t ∈ 𝒜`

from which we can remove one element
to get `s`

.

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 𝒜`

iff `t`

is exactly `k`

elements more than something in `𝒜`

.