Chvátal's Conjecture

References:

• A Conjecture in Extremal Combinatorics
• Chvátal's Conjecture and Correlation Inequalities

def Chvatal.Decreasing {α : Type} (F : Finset (Finset α)) : Prop

A family F of sets is Decreasing if it is closed under taking subsets.

Equations

• Chvatal.Decreasing F = ∀ (A B : Finset α), B ⊆ A → A ∈ F → B ∈ F

def Chvatal.Intersecting {α : Type} [DecidableEq α] (F : Finset (Finset α)) : Prop

A family F of sets is Intersecting if each pair of members has nonempty intersection.

Equations

• Chvatal.Intersecting F = ∀ A ∈ F, ∀ B ∈ F, A ∩ B ≠ ∅

theorem Chvatal.exists_maximal_star {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (F : Finset (Finset α)) : Decreasing F → ∃ (x : α), ∀ G ⊆ F, Intersecting G → G.card ≤ {A ∈ F | x ∈ A}.card

If F is a decreasing family of sets of some finite type α, then there is some element x of α such that the family consisting of all members of F containing x is an intersecting subfamily of F with maximal cardinality.