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.upShadow: 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 #

Tags #

shadow, set family

def 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 𝒜.

Equations

𝒜.shadow = 𝒜.sup fun (s : Finset α) => Finset.image s.erase 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∂» 1024 (Lean.ParserDescr.symbol "∂ ")

@[simp]

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

∅.shadow = ∅

The shadow of the empty set is empty.

@[simp]

theorem Finset.shadow_iterate_empty {α : Type u_1} [DecidableEq α] (k : ℕ) :

shadow ^[k] ∅ = ∅

@[simp]

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

{∅}.shadow = ∅

@[simp]

theorem Finset.shadow_singleton {α : Type u_1} [DecidableEq α] (a : α) :

{{a}}.shadow = {∅}

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

Monotone shadow

The shadow is monotone.

theorem Finset.shadow_mono {α : Type u_1} [DecidableEq α] {𝒜 ℬ : Finset (Finset α)} (h𝒜ℬ : 𝒜 ⊆ ℬ) :

𝒜.shadow ⊆ ℬ.shadow

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

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

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

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

s.erase a ∈ 𝒜.shadow

theorem Finset.mem_shadow_iff_exists_sdiff {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {t : Finset α} :

t ∈ 𝒜.shadow ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ (s \ t).card = 1

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

See also Finset.mem_shadow_iff_exists_mem_card_add_one.

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

t ∈ 𝒜.shadow ↔ ∃ a ∉ t, insert a t ∈ 𝒜

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

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

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

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

See also Finset.mem_shadow_iff_exists_sdiff.

theorem Finset.mem_shadow_iterate_iff_exists_card {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {t : Finset α} {k : ℕ} :

t ∈ shadow ^[k] 𝒜 ↔ ∃ (u : Finset α), u.card = k ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜

theorem Finset.mem_shadow_iterate_iff_exists_sdiff {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {t : Finset α} {k : ℕ} :

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

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

See also Finset.mem_shadow_iff_exists_mem_card_add.

theorem Finset.mem_shadow_iterate_iff_exists_mem_card_add {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {t : Finset α} {k : ℕ} :

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

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

See also Finset.mem_shadow_iterate_iff_exists_sdiff.

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

Sized (r - 1) ↑𝒜.shadow

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

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

Sized (r - k) ↑(Finset.shadow ^[k] 𝒜)

The k-th shadow of a family of r-sets is a family of r - k-sets.

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

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

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

∃ s ∈ 𝒜, t ⊆ s

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

def Finset.upShadow {α : Type u_1} [DecidableEq α] [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 (upShadow^[k]) is all sets we can get by adding k elements from any set in 𝒜.

Equations

𝒜.upShadow = 𝒜.sup fun (s : Finset α) => 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 (upShadow^[k]) is all sets we can get by adding k elements from any set in 𝒜.

Equations

FinsetFamily.«term∂⁺» = Lean.ParserDescr.node `FinsetFamily.«term∂⁺» 1024 (Lean.ParserDescr.symbol "∂⁺ ")

@[simp]

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

∅.upShadow = ∅

The upper shadow of the empty set is empty.

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

Monotone upShadow

The upper shadow is monotone.

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

t ∈ 𝒜.upShadow ↔ ∃ s ∈ 𝒜, ∃ a ∉ s, insert a s = t

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

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

insert a s ∈ 𝒜.upShadow

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

t ∈ 𝒜.upShadow ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ (t \ s).card = 1

t is in the upper shadow of 𝒜 iff t is exactly one element more than something from 𝒜.

See also Finset.mem_upShadow_iff_exists_mem_card_add_one.

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

t ∈ 𝒜.upShadow ↔ ∃ a ∈ t, t.erase 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} [DecidableEq α] [Fintype α] {𝒜 : Finset (Finset α)} {t : Finset α} :

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

t is in the upper shadow of 𝒜 iff t is exactly one element less than something from 𝒜.

See also Finset.mem_upShadow_iff_exists_sdiff.

theorem Finset.mem_upShadow_iterate_iff_exists_card {α : Type u_1} [DecidableEq α] [Fintype α] {𝒜 : Finset (Finset α)} {t : Finset α} {k : ℕ} :

t ∈ upShadow ^[k] 𝒜 ↔ ∃ (u : Finset α), u.card = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜

theorem Finset.mem_upShadow_iterate_iff_exists_sdiff {α : Type u_1} [DecidableEq α] [Fintype α] {𝒜 : Finset (Finset α)} {t : Finset α} {k : ℕ} :

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

t is in the upper shadow of 𝒜 iff t is exactly k elements less than something from 𝒜.

See also Finset.mem_upShadow_iff_exists_mem_card_add.

theorem Finset.mem_upShadow_iterate_iff_exists_mem_card_add {α : Type u_1} [DecidableEq α] [Fintype α] {𝒜 : Finset (Finset α)} {t : Finset α} {k : ℕ} :

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

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

See also Finset.mem_upShadow_iterate_iff_exists_sdiff.

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

Sized (r + 1) ↑𝒜.upShadow

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

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

∃ 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} [DecidableEq α] [Fintype α] {𝒜 : Finset (Finset α)} {s : Finset α} {k : ℕ} :

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

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

@[simp]

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

𝒜.compls.shadow = 𝒜.upShadow.compls

@[simp]

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

𝒜.compls.upShadow = 𝒜.shadow.compls