mathlib3 documentation

combinatorics.set_family.shadow

Shadows #

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.

Notation #

We define notation in locale finset_family:

∂ 𝒜: 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} [decidable_eq α] (𝒜 : 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 (λ (s : finset α), finset.image s.erase s)

@[simp]

theorem finset.shadow_empty {α : Type u_1} [decidable_eq α] :

∅.shadow = ∅

The shadow of the empty set is empty.

@[simp]

theorem finset.shadow_singleton_empty {α : Type u_1} [decidable_eq α] :

{∅}.shadow = ∅

theorem finset.shadow_monotone {α : Type u_1} [decidable_eq α] :

monotone finset.shadow

The shadow is monotone.

theorem finset.mem_shadow_iff {α : Type u_1} [decidable_eq α] {𝒜 : finset (finset α)} {s : finset α} :

s ∈ 𝒜.shadow ↔ ∃ (t : finset α) (H : t ∈ 𝒜) (a : α) (H : a ∈ t), t.erase 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} [decidable_eq α] {𝒜 : finset (finset α)} {s : finset α} {a : α} (hs : s ∈ 𝒜) (ha : a ∈ s) :

s.erase a ∈ 𝒜.shadow

theorem finset.mem_shadow_iff_insert_mem {α : Type u_1} [decidable_eq α] {𝒜 : finset (finset α)} {s : finset α} :

s ∈ 𝒜.shadow ↔ ∃ (a : α) (H : a ∉ s), has_insert.insert a s ∈ 𝒜

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

@[protected]

theorem set.sized.shadow {α : Type u_1} [decidable_eq α] {𝒜 : finset (finset α)} {r : ℕ} (h𝒜 : set.sized r ↑𝒜) :

set.sized (r - 1) ↑(𝒜.shadow)

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

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

set.sized r ↑(𝒜.shadow) ↔ set.sized (r + 1) ↑𝒜

theorem finset.mem_shadow_iff_exists_mem_card_add_one {α : Type u_1} [decidable_eq α] {𝒜 : finset (finset α)} {s : finset α} :

s ∈ 𝒜.shadow ↔ ∃ (t : finset α) (H : t ∈ 𝒜), s ⊆ t ∧ t.card = s.card + 1

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

theorem finset.exists_subset_of_mem_shadow {α : Type u_1} [decidable_eq α] {𝒜 : finset (finset α)} {s : finset α} (hs : s ∈ 𝒜.shadow) :

∃ (t : finset α) (H : 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} [decidable_eq α] {𝒜 : finset (finset α)} {s : finset α} {k : ℕ} :

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

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

def finset.up_shadow {α : Type u_1} [decidable_eq α] [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

𝒜.up_shadow = 𝒜.sup (λ (s : finset α), finset.image (λ (a : α), has_insert.insert a s) sᶜ)

@[simp]

theorem finset.up_shadow_empty {α : Type u_1} [decidable_eq α] [fintype α] :

∅.up_shadow = ∅

The upper shadow of the empty set is empty.

theorem finset.up_shadow_monotone {α : Type u_1} [decidable_eq α] [fintype α] :

monotone finset.up_shadow

The upper shadow is monotone.

theorem finset.mem_up_shadow_iff {α : Type u_1} [decidable_eq α] [fintype α] {𝒜 : finset (finset α)} {s : finset α} :

s ∈ 𝒜.up_shadow ↔ ∃ (t : finset α) (H : t ∈ 𝒜) (a : α) (H : a ∉ t), has_insert.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_up_shadow {α : Type u_1} [decidable_eq α] [fintype α] {𝒜 : finset (finset α)} {s : finset α} {a : α} (hs : s ∈ 𝒜) (ha : a ∉ s) :

has_insert.insert a s ∈ 𝒜.up_shadow

@[protected]

theorem set.sized.up_shadow {α : Type u_1} [decidable_eq α] [fintype α] {𝒜 : finset (finset α)} {r : ℕ} (h𝒜 : set.sized r ↑𝒜) :

set.sized (r + 1) ↑(𝒜.up_shadow)

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

theorem finset.mem_up_shadow_iff_erase_mem {α : Type u_1} [decidable_eq α] [fintype α] {𝒜 : finset (finset α)} {s : finset α} :

s ∈ 𝒜.up_shadow ↔ ∃ (a : α) (H : a ∈ s), s.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_up_shadow_iff_exists_mem_card_add_one {α : Type u_1} [decidable_eq α] [fintype α] {𝒜 : finset (finset α)} {s : finset α} :

s ∈ 𝒜.up_shadow ↔ ∃ (t : finset α) (H : t ∈ 𝒜), t ⊆ s ∧ t.card + 1 = s.card

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

theorem finset.exists_subset_of_mem_up_shadow {α : Type u_1} [decidable_eq α] [fintype α] {𝒜 : finset (finset α)} {s : finset α} (hs : s ∈ 𝒜.up_shadow) :

∃ (t : finset α) (H : t ∈ 𝒜), t ⊆ s

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

theorem finset.mem_up_shadow_iff_exists_mem_card_add {α : Type u_1} [decidable_eq α] [fintype α] {𝒜 : finset (finset α)} {s : finset α} {k : ℕ} :

s ∈ finset.up_shadow ^[k] 𝒜 ↔ ∃ (t : finset α) (H : t ∈ 𝒜), t ⊆ s ∧ t.card + k = s.card

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

@[simp]

theorem finset.shadow_image_compl {α : Type u_1} [decidable_eq α] [fintype α] {𝒜 : finset (finset α)} :

finset.image has_compl.compl 𝒜.shadow = (finset.image has_compl.compl 𝒜).up_shadow

@[simp]

theorem finset.up_shadow_image_compl {α : Type u_1} [decidable_eq α] [fintype α] {𝒜 : finset (finset α)} :

finset.image has_compl.compl 𝒜.up_shadow = (finset.image has_compl.compl 𝒜).shadow