Intersecting families with large cover number

DefinitionErdős–Lovász family#✓fully proved

For a natural number \(n\), a finite family \(\mathcal{F}\) of finite sets of natural numbers is an Erdős–Lovász family of order \(n\) when every member of \(\mathcal{F}\) has exactly \(n\) elements, any two members of \(\mathcal{F}\) (not necessarily distinct) have a common element, and every set of at most \(n - 1\) natural numbers is disjoint from some member of \(\mathcal{F}\), where \(n - 1\) is read as \(0\) when \(n = 0\).

def IsErdosLovaszFamily (n : ℕ) (F : Finset (Finset ℕ)) : Prop :=
  (∀ A ∈ F, A.card = n) ∧ (∀ A ∈ F, ∀ B ∈ F, (A ∩ B).Nonempty) ∧
    ∀ S : Finset ℕ, S.card ≤ n - 1 → ∃ A ∈ F, Disjoint S A

Used by 1

Used byErdős Problem 21 (Erdős–Lovász)

DefinitionErdős Problem 21 (Erdős–Lovász)#✓fully proved

The statement that there is a natural number \(C\) such that for every \(n \ge 1\) there is a finite family \(\mathcal{F}\) of finite sets of natural numbers in which every member has exactly \(n\) elements, any two members have a common element, every set of at most \(n - 1\) natural numbers is disjoint from some member, and \(|\mathcal{F}| \le C n\). This expresses \(f(n) \ll n\), where \(f(n)\) is the least size of such a family.

def intersectingFamilyFullCoverLinearSize : Prop :=
  ∃ C : ℕ, ∀ n : ℕ, 1 ≤ n → ∃ F : Finset (Finset ℕ), IsErdosLovaszFamily n F ∧ F.card ≤ C * n

Uses 1 · Used by 1

Statement usesErdős–Lovász family

Used byKahn's theorem on the Erdős–Lovász problem

TheoremKahn's theorem on the Erdős–Lovász problem#●ready to prove

There is a natural number \(C\) such that for every \(n \ge 1\) there is a finite family \(\mathcal{F}\) of finite sets of natural numbers with the following properties: every member of \(\mathcal{F}\) has exactly \(n\) elements, any two members of \(\mathcal{F}\) have a common element, every set of at most \(n - 1\) natural numbers is disjoint from some member of \(\mathcal{F}\), and \(|\mathcal{F}| \le C n\).

Kahn proved this, improving his earlier bound \(O(n \log n)\) obtained from random lines in projective planes; it answers Erdős Problem 21 in the affirmative.

public theorem_wanted intersectingFamilyFullCoverLinearSize_holds :
    intersectingFamilyFullCoverLinearSize

Sources

• T. F. Bloom, Erdős Problems, Problem #21, https://www.erdosproblems.com/21 (status PROVED (LEAN)); resolution: J. Kahn, On a problem of Erdős and Lovász. II. n(r) = O(r), J. Amer. Math. Soc. 7 (1994), 125-143, main theorem n(r) = O(r); erdosproblems.com/21: solved by Kahn [Ka94], https://doi.org/10.2307/2152722.

Uses 1

Statement usesErdős Problem 21 (Erdős–Lovász)

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.