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 #

Notation #

We define notation in locale FinsetFamily:

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 α)) :

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
      @[simp]

      The shadow of the empty set is empty.

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

      The shadow is monotone.

      theorem Finset.mem_shadow_iff {α : Type u_1} [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 a t ∈ 𝒜 from which we can remove one element to get s.

      theorem Finset.erase_mem_shadow {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} {a : α} (hs : s 𝒜) (ha : a s) :
      theorem Finset.mem_shadow_iff_insert_mem {α : Type u_1} [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} [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} [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} [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} [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} [DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} {k : } :
      s Finset.shadow^[k] 𝒜 t, t 𝒜 s t Finset.card t = Finset.card s + k

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

      def Finset.upShadow {α : Type u_1} [DecidableEq α] [Fintype α] (𝒜 : 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 𝒜.

      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
          @[simp]

          The upper shadow of the empty set is empty.

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

          The upper shadow is monotone.

          theorem Finset.mem_upShadow_iff {α : Type u_1} [DecidableEq α] [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 a t ∈ 𝒜 from which we can remove one element to get s.

          theorem Finset.insert_mem_upShadow {α : Type u_1} [DecidableEq α] [Fintype α] {𝒜 : Finset (Finset α)} {s : Finset α} {a : α} (hs : s 𝒜) (ha : ¬a s) :
          theorem Finset.Set.Sized.upShadow {α : Type u_1} [DecidableEq α] [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} [DecidableEq α] [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} [DecidableEq α] [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} [DecidableEq α] [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} [DecidableEq α] [Fintype α] {𝒜 : Finset (Finset α)} {s : Finset α} {k : } :
          s Finset.upShadow^[k] 𝒜 t, t 𝒜 t s Finset.card t + k = Finset.card s

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

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