Documentation

Mathlib.Combinatorics.SetFamily.Shadow

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

def Finset.shadow {α : Type u_1} [inst : 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 𝒜.

Equations

Finset.shadow 𝒜 = Finset.sup 𝒜 fun s => Finset.image (Finset.erase s) s

def FinsetFamily.«term∂» :

Lean.ParserDescr

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 "∂ ")

@[simp]

theorem Finset.shadow_empty {α : Type u_1} [inst : DecidableEq α] :

Finset.shadow ∅ = ∅

The shadow of the empty set is empty.

@[simp]

theorem Finset.shadow_singleton_empty {α : Type u_1} [inst : DecidableEq α] :

Finset.shadow {∅} = ∅

theorem Finset.shadow_monotone {α : Type u_1} [inst : DecidableEq α] :

Monotone Finset.shadow

The shadow is monotone.

theorem Finset.mem_shadow_iff {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} :

s ∈ Finset.shadow 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ ∃ a, a ∈ t ∧ Finset.erase t a = s

s is in the shadow of 𝒜 iff there is an t ∈ 𝒜∈ 𝒜 from which we can remove one element to get s.

theorem Finset.erase_mem_shadow {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} {a : α} (hs : s ∈ 𝒜) (ha : a ∈ s) :

Finset.erase s a ∈ Finset.shadow 𝒜

theorem Finset.mem_shadow_iff_insert_mem {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} :

s ∈ Finset.shadow 𝒜 ↔ ∃ a x, insert a s ∈ 𝒜

t is in the shadow of 𝒜 iff we can add an element to it so that the resulting finset is in 𝒜.

theorem Finset.Set.Sized.shadow {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {r : ℕ} (h𝒜 : Set.Sized r ↑𝒜) :

Set.Sized (r - 1) ↑(Finset.shadow 𝒜)

The shadow of a family of r-sets is a family of r - 1-sets.

theorem Finset.sized_shadow_iff {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {r : ℕ} (h : ¬∅ ∈ 𝒜) :

Set.Sized r ↑(Finset.shadow 𝒜) ↔ Set.Sized (r + 1) ↑𝒜

theorem Finset.mem_shadow_iff_exists_mem_card_add_one {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} :

s ∈ Finset.shadow 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ Finset.card t = Finset.card s + 1

s ∈ ∂ 𝒜∈ ∂ 𝒜∂ 𝒜 iff s is exactly one element less than something from 𝒜

theorem Finset.exists_subset_of_mem_shadow {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} (hs : s ∈ Finset.shadow 𝒜) :

∃ t, t ∈ 𝒜 ∧ s ⊆ t

Being in the shadow of 𝒜 means we have a superset in 𝒜.

theorem Finset.mem_shadow_iff_exists_mem_card_add {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} {k : ℕ} :

s ∈ (Finset.shadow ^[k]) 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ Finset.card t = Finset.card s + k

t ∈ ∂^k 𝒜∈ ∂^k 𝒜∂^k 𝒜 iff t is exactly k elements less than something in 𝒜.

def Finset.upShadow {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] (𝒜 : Finset (Finset α)) :

Finset (Finset α)

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ᶜ)

def FinsetFamily.«term∂⁺» :

Lean.ParserDescr

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 "∂⁺ ")

@[simp]

theorem Finset.upShadow_empty {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] :

Finset.upShadow ∅ = ∅

The upper shadow of the empty set is empty.

theorem Finset.upShadow_monotone {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] :

Monotone Finset.upShadow

The upper shadow is monotone.

theorem Finset.mem_upShadow_iff {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] {𝒜 : Finset (Finset α)} {s : Finset α} :

s ∈ Finset.upShadow 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ ∃ a x, insert a t = s

s is in the upper shadow of 𝒜 iff there is an t ∈ 𝒜∈ 𝒜 from which we can remove one element to get s.

theorem Finset.insert_mem_upShadow {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] {𝒜 : Finset (Finset α)} {s : Finset α} {a : α} (hs : s ∈ 𝒜) (ha : ¬a ∈ s) :

insert a s ∈ Finset.upShadow 𝒜

theorem Finset.Set.Sized.upShadow {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] {𝒜 : Finset (Finset α)} {r : ℕ} (h𝒜 : Set.Sized r ↑𝒜) :

Set.Sized (r + 1) ↑(Finset.upShadow 𝒜)

The upper shadow of a family of r-sets is a family of r + 1-sets.

theorem Finset.mem_upShadow_iff_erase_mem {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] {𝒜 : Finset (Finset α)} {s : Finset α} :

s ∈ Finset.upShadow 𝒜 ↔ ∃ a, a ∈ s ∧ Finset.erase s a ∈ 𝒜

t is in the upper shadow of 𝒜 iff we can remove an element from it so that the resulting finset is in 𝒜.

theorem Finset.mem_upShadow_iff_exists_mem_card_add_one {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] {𝒜 : Finset (Finset α)} {s : Finset α} :

s ∈ Finset.upShadow 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ Finset.card t + 1 = Finset.card s

s ∈ ∂⁺ 𝒜∈ ∂⁺ 𝒜∂⁺ 𝒜⁺ 𝒜 iff s is exactly one element less than something from 𝒜.

theorem Finset.exists_subset_of_mem_upShadow {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] {𝒜 : Finset (Finset α)} {s : Finset α} (hs : s ∈ Finset.upShadow 𝒜) :

∃ t, t ∈ 𝒜 ∧ t ⊆ s

Being in the upper shadow of 𝒜 means we have a superset in 𝒜.

theorem Finset.mem_upShadow_iff_exists_mem_card_add {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] {𝒜 : Finset (Finset α)} {s : Finset α} {k : ℕ} :

s ∈ (Finset.upShadow ^[k]) 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ Finset.card t + k = Finset.card s

t ∈ ∂^k 𝒜∈ ∂^k 𝒜∂^k 𝒜 iff t is exactly k elements more than something in 𝒜.

@[simp]

theorem Finset.shadow_image_compl {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] {𝒜 : Finset (Finset α)} :

Finset.image compl (Finset.shadow 𝒜) = Finset.upShadow (Finset.image compl 𝒜)

@[simp]

theorem Finset.upShadow_image_compl {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] {𝒜 : Finset (Finset α)} :

Finset.image compl (Finset.upShadow 𝒜) = Finset.shadow (Finset.image compl 𝒜)