Documentation

Mathlib.Combinatorics.SetFamily.Compression.Down

Down-compressions #

This file defines down-compression.

Down-compressing π’œ : Finset (Finset Ξ±) along a : Ξ± means removing a from the elements of π’œ, when the resulting set is not already in π’œ.

Main declarations #

Notation #

𝓓 a π’œ is notation for Down.compress a π’œ in scope SetFamily.

References #

Tags #

compression, down-compression

source
def Finset.nonMemberSubfamily {Ξ± : Type u_1} [DecidableEq Ξ±] (a : Ξ±) (π’œ : Finset (Finset Ξ±)) :
Finset (Finset Ξ±)

Elements of π’œ that do not contain a.

Equations
Instances For
    source
    def Finset.memberSubfamily {Ξ± : Type u_1} [DecidableEq Ξ±] (a : Ξ±) (π’œ : Finset (Finset Ξ±)) :
    Finset (Finset Ξ±)

    Image of the elements of π’œ which contain a under removing a. Finsets that do not contain a such that insert a s ∈ π’œ.

    Equations
    Instances For
      source
      @[simp]
      theorem Finset.mem_nonMemberSubfamily {Ξ± : Type u_1} [DecidableEq Ξ±] {π’œ : Finset (Finset Ξ±)} {s : Finset Ξ±} {a : Ξ±} :
      s ∈ nonMemberSubfamily a π’œ ↔ s ∈ π’œ ∧ a βˆ‰ s
      source
      @[simp]
      theorem Finset.mem_memberSubfamily {Ξ± : Type u_1} [DecidableEq Ξ±] {π’œ : Finset (Finset Ξ±)} {s : Finset Ξ±} {a : Ξ±} :
      s ∈ memberSubfamily a π’œ ↔ insert a s ∈ π’œ ∧ a βˆ‰ s
      source
      theorem Finset.nonMemberSubfamily_inter {Ξ± : Type u_1} [DecidableEq Ξ±] (a : Ξ±) (π’œ ℬ : Finset (Finset Ξ±)) :
      nonMemberSubfamily a (π’œ ∩ ℬ) = nonMemberSubfamily a π’œ ∩ nonMemberSubfamily a ℬ
      source
      theorem Finset.memberSubfamily_inter {Ξ± : Type u_1} [DecidableEq Ξ±] (a : Ξ±) (π’œ ℬ : Finset (Finset Ξ±)) :
      memberSubfamily a (π’œ ∩ ℬ) = memberSubfamily a π’œ ∩ memberSubfamily a ℬ
      source
      theorem Finset.nonMemberSubfamily_union {Ξ± : Type u_1} [DecidableEq Ξ±] (a : Ξ±) (π’œ ℬ : Finset (Finset Ξ±)) :
      nonMemberSubfamily a (π’œ βˆͺ ℬ) = nonMemberSubfamily a π’œ βˆͺ nonMemberSubfamily a ℬ
      source
      theorem Finset.memberSubfamily_union {Ξ± : Type u_1} [DecidableEq Ξ±] (a : Ξ±) (π’œ ℬ : Finset (Finset Ξ±)) :
      memberSubfamily a (π’œ βˆͺ ℬ) = memberSubfamily a π’œ βˆͺ memberSubfamily a ℬ
      source
      theorem Finset.card_memberSubfamily_add_card_nonMemberSubfamily {Ξ± : Type u_1} [DecidableEq Ξ±] (a : Ξ±) (π’œ : Finset (Finset Ξ±)) :
      (memberSubfamily a π’œ).card + (nonMemberSubfamily a π’œ).card = π’œ.card
      source
      theorem Finset.memberSubfamily_union_nonMemberSubfamily {Ξ± : Type u_1} [DecidableEq Ξ±] (a : Ξ±) (π’œ : Finset (Finset Ξ±)) :
      memberSubfamily a π’œ βˆͺ nonMemberSubfamily a π’œ = image (fun (s : Finset Ξ±) => s.erase a) π’œ
      source
      @[simp]
      theorem Finset.memberSubfamily_memberSubfamily {Ξ± : Type u_1} [DecidableEq Ξ±] {π’œ : Finset (Finset Ξ±)} {a : Ξ±} :
      memberSubfamily a (memberSubfamily a π’œ) = βˆ…
      source
      @[simp]
      theorem Finset.memberSubfamily_nonMemberSubfamily {Ξ± : Type u_1} [DecidableEq Ξ±] {π’œ : Finset (Finset Ξ±)} {a : Ξ±} :
      memberSubfamily a (nonMemberSubfamily a π’œ) = βˆ…
      source
      @[simp]
      theorem Finset.nonMemberSubfamily_memberSubfamily {Ξ± : Type u_1} [DecidableEq Ξ±] {π’œ : Finset (Finset Ξ±)} {a : Ξ±} :
      nonMemberSubfamily a (memberSubfamily a π’œ) = memberSubfamily a π’œ
      source
      @[simp]
      theorem Finset.nonMemberSubfamily_nonMemberSubfamily {Ξ± : Type u_1} [DecidableEq Ξ±] {π’œ : Finset (Finset Ξ±)} {a : Ξ±} :
      nonMemberSubfamily a (nonMemberSubfamily a π’œ) = nonMemberSubfamily a π’œ
      source
      theorem Finset.memberSubfamily_image_insert {Ξ± : Type u_1} [DecidableEq Ξ±] {π’œ : Finset (Finset Ξ±)} {a : Ξ±} (hπ’œ : βˆ€ s ∈ π’œ, a βˆ‰ s) :
      memberSubfamily a (image (insert a) π’œ) = π’œ
      source
      @[simp]
      theorem Finset.nonMemberSubfamily_image_insert {Ξ± : Type u_1} [DecidableEq Ξ±] {π’œ : Finset (Finset Ξ±)} {a : Ξ±} :
      nonMemberSubfamily a (image (insert a) π’œ) = βˆ…
      source
      @[simp]
      theorem Finset.memberSubfamily_image_erase {Ξ± : Type u_1} [DecidableEq Ξ±] {π’œ : Finset (Finset Ξ±)} {a : Ξ±} :
      memberSubfamily a (image (fun (x : Finset Ξ±) => x.erase a) π’œ) = βˆ…
      source
      theorem Finset.image_insert_memberSubfamily {Ξ± : Type u_1} [DecidableEq Ξ±] (π’œ : Finset (Finset Ξ±)) (a : Ξ±) :
      image (insert a) (memberSubfamily a π’œ) = {s ∈ π’œ | a ∈ s}
      source
      theorem Finset.memberFamily_induction_on {Ξ± : Type u_1} [DecidableEq Ξ±] {p : Finset (Finset Ξ±) β†’ Prop} (π’œ : Finset (Finset Ξ±)) (empty : p βˆ…) (singleton_empty : p {βˆ…}) (subfamily : βˆ€ (a : Ξ±) β¦ƒπ’œ : Finset (Finset Ξ±)⦄, p (nonMemberSubfamily a π’œ) β†’ p (memberSubfamily a π’œ) β†’ p π’œ) :
      p π’œ

      Induction principle for finset families. To prove a statement for every finset family, it suffices to prove it for

      • the empty finset family.
      • the finset family which only contains the empty finset.
      • ℬ βˆͺ {s βˆͺ {a} | s ∈ π’ž} assuming the property for ℬ and π’ž, where a is an element of the ground type and π’œ and ℬ are families of finsets not containing a. Note that instead of giving ℬ and π’ž, the subfamily case gives you π’œ = ℬ βˆͺ {s βˆͺ {a} | s ∈ π’ž}, so that ℬ = π’œ.nonMemberSubfamily and π’ž = π’œ.memberSubfamily.

      This is a way of formalising induction on n where π’œ is a finset family on n elements.

      See also Finset.family_induction_on.

      source
      theorem Finset.family_induction_on {Ξ± : Type u_1} [DecidableEq Ξ±] {p : Finset (Finset Ξ±) β†’ Prop} (π’œ : Finset (Finset Ξ±)) (empty : p βˆ…) (singleton_empty : p {βˆ…}) (image_insert : βˆ€ (a : Ξ±) β¦ƒπ’œ : Finset (Finset Ξ±)⦄, (βˆ€ s ∈ π’œ, a βˆ‰ s) β†’ p π’œ β†’ p (image (insert a) π’œ)) (subfamily : βˆ€ (a : Ξ±) β¦ƒπ’œ : Finset (Finset Ξ±)⦄, p ({s ∈ π’œ | a βˆ‰ s}) β†’ p ({s ∈ π’œ | a ∈ s}) β†’ p π’œ) :
      p π’œ

      Induction principle for finset families. To prove a statement for every finset family, it suffices to prove it for

      • the empty finset family.
      • the finset family which only contains the empty finset.
      • {s βˆͺ {a} | s ∈ π’œ} assuming the property for π’œ a family of finsets not containing a.
      • ℬ βˆͺ π’ž assuming the property for ℬ and π’ž, where a is an element of the ground type and ℬis a family of finsets not containing a and π’ž a family of finsets containing a. Note that instead of giving ℬ and π’ž, the subfamily case gives you π’œ = ℬ βˆͺ π’ž, so that ℬ = {s ∈ π’œ | a βˆ‰ s} and π’ž = {s ∈ π’œ | a ∈ s}.

      This is a way of formalising induction on n where π’œ is a finset family on n elements.

      See also Finset.memberFamily_induction_on.

      source
      def Down.compression {Ξ± : Type u_1} [DecidableEq Ξ±] (a : Ξ±) (π’œ : Finset (Finset Ξ±)) :
      Finset (Finset Ξ±)

      a-down-compressing π’œ means removing a from the elements of π’œ that contain it, when the resulting Finset is not already in π’œ.

      Equations
      Instances For
        source
        def FinsetFamily.term𝓓 :
        Lean.ParserDescr

        a-down-compressing π’œ means removing a from the elements of π’œ that contain it, when the resulting Finset is not already in π’œ.

        Equations
        Instances For
          source
          theorem Down.mem_compression {Ξ± : Type u_1} [DecidableEq Ξ±] {π’œ : Finset (Finset Ξ±)} {s : Finset Ξ±} {a : Ξ±} :
          s ∈ compression a π’œ ↔ s ∈ π’œ ∧ s.erase a ∈ π’œ ∨ s βˆ‰ π’œ ∧ insert a s ∈ π’œ

          a is in the down-compressed family iff it's in the original and its compression is in the original, or it's not in the original but it's the compression of something in the original.

          source
          theorem Down.erase_mem_compression {Ξ± : Type u_1} [DecidableEq Ξ±] {π’œ : Finset (Finset Ξ±)} {s : Finset Ξ±} {a : Ξ±} (hs : s ∈ π’œ) :
          s.erase a ∈ compression a π’œ
          source
          theorem Down.erase_mem_compression_of_mem_compression {Ξ± : Type u_1} [DecidableEq Ξ±] {π’œ : Finset (Finset Ξ±)} {s : Finset Ξ±} {a : Ξ±} :
          s ∈ compression a π’œ β†’ s.erase a ∈ compression a π’œ
          source
          theorem Down.mem_compression_of_insert_mem_compression {Ξ± : Type u_1} [DecidableEq Ξ±] {π’œ : Finset (Finset Ξ±)} {s : Finset Ξ±} {a : Ξ±} (h : insert a s ∈ compression a π’œ) :
          s ∈ compression a π’œ
          source
          @[simp]
          theorem Down.compression_idem {Ξ± : Type u_1} [DecidableEq Ξ±] (a : Ξ±) (π’œ : Finset (Finset Ξ±)) :
          compression a (compression a π’œ) = compression a π’œ

          Down-compressing a family is idempotent.

          source
          @[simp]
          theorem Down.card_compression {Ξ± : Type u_1} [DecidableEq Ξ±] (a : Ξ±) (π’œ : Finset (Finset Ξ±)) :
          (compression a π’œ).card = π’œ.card

          Down-compressing a family doesn't change its size.