Sunflowers

This file defines sunflowers of set families.

def IsSunflowerWithKernel {α : Type u_1} (F : Set (Set α)) (S : Set α) : Prop

A sunflower F with kernel S is a collection of sets in which all possible distinct pairs of sets share the same intersection S.

Equations

• IsSunflowerWithKernel F S = F.Pairwise fun (A B : Set α) => A ∩ B = S

theorem isSunflowerWithKernel_empty {α : Type u_1} (S : Set α) : IsSunflowerWithKernel ∅ S

theorem isSunflowerWithKernel_singleton {α : Type u_1} (S A : Set α) : IsSunflowerWithKernel {A} S

def IsSunflower {α : Type u_1} (F : Set (Set α)) : Prop

A sunflower F is a collection of sets in which all possible distinct pairs of sets share the same intersection.

Equations

• IsSunflower F = ∃ (S : Set α), IsSunflowerWithKernel F S

theorem isSunflower_empty {α : Type u_1} : IsSunflower ∅

theorem isSunflower_singleton {α : Type u_1} (A : Set α) : IsSunflower {A}