Down-compressions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

finset.non_member_subfamily: 𝒜.non_member_subfamily a is the subfamily of sets not containing a.
finset.member_subfamily: 𝒜.member_subfamily a is the image of the subfamily of sets containing a under removing a.
down.compression: Down-compression.

Notation #

𝓓 a 𝒜 is notation for down.compress a 𝒜 in locale set_family.

References #

https://github.com/b-mehta/maths-notes/blob/master/iii/mich/combinatorics.pdf

Tags #

compression, down-compression

source

def finset.non_member_subfamily {α : Type u_1} [decidable_eq α] (a : α) (𝒜 : finset (finset α)) :

finset (finset α)

Elements of 𝒜 that do not contain a.

Equations

finset.non_member_subfamily a 𝒜 = finset.filter (λ (s : finset α), a ∉ s) 𝒜

source

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

finset.member_subfamily a 𝒜 = finset.image (λ (s : finset α), s.erase a) (finset.filter (λ (s : finset α), a ∈ s) 𝒜)

source

@[simp]

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

s ∈ finset.non_member_subfamily a 𝒜 ↔ s ∈ 𝒜 ∧ a ∉ s

source

@[simp]

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

s ∈ finset.member_subfamily a 𝒜 ↔ has_insert.insert a s ∈ 𝒜 ∧ a ∉ s

source

theorem finset.non_member_subfamily_inter {α : Type u_1} [decidable_eq α] (a : α) (𝒜 ℬ : finset (finset α)) :

finset.non_member_subfamily a (𝒜 ∩ ℬ) = finset.non_member_subfamily a 𝒜 ∩ finset.non_member_subfamily a ℬ

source

theorem finset.member_subfamily_inter {α : Type u_1} [decidable_eq α] (a : α) (𝒜 ℬ : finset (finset α)) :

finset.member_subfamily a (𝒜 ∩ ℬ) = finset.member_subfamily a 𝒜 ∩ finset.member_subfamily a ℬ

source

theorem finset.non_member_subfamily_union {α : Type u_1} [decidable_eq α] (a : α) (𝒜 ℬ : finset (finset α)) :

finset.non_member_subfamily a (𝒜 ∪ ℬ) = finset.non_member_subfamily a 𝒜 ∪ finset.non_member_subfamily a ℬ

source

theorem finset.member_subfamily_union {α : Type u_1} [decidable_eq α] (a : α) (𝒜 ℬ : finset (finset α)) :

finset.member_subfamily a (𝒜 ∪ ℬ) = finset.member_subfamily a 𝒜 ∪ finset.member_subfamily a ℬ

source

theorem finset.card_member_subfamily_add_card_non_member_subfamily {α : Type u_1} [decidable_eq α] (a : α) (𝒜 : finset (finset α)) :

(finset.member_subfamily a 𝒜).card + (finset.non_member_subfamily a 𝒜).card = 𝒜.card

source

theorem finset.member_subfamily_union_non_member_subfamily {α : Type u_1} [decidable_eq α] (a : α) (𝒜 : finset (finset α)) :

finset.member_subfamily a 𝒜 ∪ finset.non_member_subfamily a 𝒜 = finset.image (λ (s : finset α), s.erase a) 𝒜

source

@[simp]

theorem finset.member_subfamily_member_subfamily {α : Type u_1} [decidable_eq α] {𝒜 : finset (finset α)} {a : α} :

finset.member_subfamily a (finset.member_subfamily a 𝒜) = ∅

source

@[simp]

theorem finset.member_subfamily_non_member_subfamily {α : Type u_1} [decidable_eq α] {𝒜 : finset (finset α)} {a : α} :

finset.member_subfamily a (finset.non_member_subfamily a 𝒜) = ∅

source

@[simp]

theorem finset.non_member_subfamily_member_subfamily {α : Type u_1} [decidable_eq α] {𝒜 : finset (finset α)} {a : α} :

finset.non_member_subfamily a (finset.member_subfamily a 𝒜) = finset.member_subfamily a 𝒜

source

@[simp]

theorem finset.non_member_subfamily_non_member_subfamily {α : Type u_1} [decidable_eq α] {𝒜 : finset (finset α)} {a : α} :

finset.non_member_subfamily a (finset.non_member_subfamily a 𝒜) = finset.non_member_subfamily a 𝒜

source

def down.compression {α : Type u_1} [decidable_eq α] (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

down.compression a 𝒜 = (finset.filter (λ (s : finset α), s.erase a ∈ 𝒜) 𝒜).disj_union (finset.filter (λ (s : finset α), s ∉ 𝒜) (finset.image (λ (s : finset α), s.erase a) 𝒜)) _

source

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

s ∈ down.compression a 𝒜 ↔ s ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ s ∉ 𝒜 ∧ has_insert.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} [decidable_eq α] {𝒜 : finset (finset α)} {s : finset α} {a : α} (hs : s ∈ 𝒜) :

s.erase a ∈ down.compression a 𝒜

source

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

s ∈ down.compression a 𝒜 → s.erase a ∈ down.compression a 𝒜

source

theorem down.mem_compression_of_insert_mem_compression {α : Type u_1} [decidable_eq α] {𝒜 : finset (finset α)} {s : finset α} {a : α} (h : has_insert.insert a s ∈ down.compression a 𝒜) :

s ∈ down.compression a 𝒜

source

@[simp]

theorem down.compression_idem {α : Type u_1} [decidable_eq α] (a : α) (𝒜 : finset (finset α)) :

down.compression a (down.compression a 𝒜) = down.compression a 𝒜

Down-compressing a family is idempotent.

source

@[simp]

theorem down.card_compression {α : Type u_1} [decidable_eq α] (a : α) (𝒜 : finset (finset α)) :

(down.compression a 𝒜).card = 𝒜.card

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