The sunflower lemma

A family of sets is a sunflower with core K when any two distinct members intersect exactly in K. The Erdős–Rado sunflower lemma says that a family of more than (p - 1) ^ w * w! sets, each of at most w elements, contains a sunflower with p petals Erdős and Rado.

The proof takes a maximal subfamily of pairwise disjoint sets. If it has p members, it is a sunflower with empty core. Otherwise its union is small and meets every nonempty set of the family, so some point lies in many sets; removing that point from them and applying the lemma for size w - 1 gives a sunflower, and putting the point back gives one for the family.

Main definitions

• Cslib.IsSunflower, Cslib.ContainsSunflower.
• Cslib.sunflowerBound: (p - 1) ^ w * w!.

Main results

• Cslib.containsSunflower_of_forall_card_le: the sunflower lemma.

References

• P. Erdős, R. Rado, Intersection theorems for systems of sets

def Cslib.IsSunflower {α : Type u_1} [DecidableEq α] (S : Finset (Finset α)) (K : Finset α) : Prop

S is a sunflower with core K: any two distinct members of S intersect exactly in K.

def Cslib.ContainsSunflower {α : Type u_1} [DecidableEq α] (p : ℕ) (F : Finset (Finset α)) : Prop

F contains a sunflower with p petals.

def Cslib.sunflowerBound (p w : ℕ) : ℕ

The bound of the sunflower lemma for sets of size at most w: (p - 1) ^ w * w!.

theorem Cslib.sunflowerBound_pos {p : ℕ} (hp : 2 ≤ p) (w : ℕ) : 0 < sunflowerBound p w

The sunflower bound is positive when 2 ≤ p.

theorem Cslib.IsSunflower.mono {α : Type u_1} [DecidableEq α] {S T : Finset (Finset α)} {K : Finset α} (h : IsSunflower T K) (hST : S ⊆ T) : IsSunflower S K

A subfamily of a sunflower with core K is a sunflower with core K.

theorem Cslib.IsSunflower.subset_of_mem {α : Type u_1} [DecidableEq α] {S : Finset (Finset α)} {K s : Finset α} (h : IsSunflower S K) (hS : 2 ≤ S.card) (hs : s ∈ S) : K ⊆ s

The core of a sunflower with at least two petals is contained in every petal.

theorem Cslib.isSunflower_empty_of_pairwise_disjoint {α : Type u_1} [DecidableEq α] {S : Finset (Finset α)} (h : (↑S).Pairwise Disjoint) : IsSunflower S ∅

Pairwise disjoint sets form a sunflower with empty core.

theorem Cslib.IsSunflower.image_insert {α : Type u_1} [DecidableEq α] {S : Finset (Finset α)} {K : Finset α} (h : IsSunflower S K) (x : α) : IsSunflower (Finset.image (insert x) S) (insert x K)

Adding a point outside all members to every member of a sunflower gives a sunflower.

theorem Cslib.containsSunflower_of_forall_card_le {α : Type u_1} [DecidableEq α] (p w : ℕ) (F : Finset (Finset α)) (hF : ∀ s ∈ F, s.card ≤ w) (hlarge : sunflowerBound p w < F.card) : ContainsSunflower p F

The sunflower lemma Erdős and Rado. A family of more than (p - 1) ^ w * w! sets of at most w elements contains a sunflower with p petals.