Families with no singleton intersection

DefinitionErdős Problem 702 on singleton intersections#✓fully proved

For every \(k \ge 4\) and every sufficiently large \(n\) (depending on \(k\)), every family of more than \(\binom{n-2}{k-2}\) subsets of \(\{1, \dots, n\}\), each with exactly \(k\) elements, contains two sets \(A\) and \(B\) with \(|A \cap B| = 1\).

This is Frankl's form of the problem of Erdős and Sós; without the hypothesis that \(n\) is large the statement fails, for instance for \(k = 4\) and \(n = 5\).

def noSingletonIntersectionBound : Prop :=
  ∀ k : ℕ, 4 ≤ k → ∀ᶠ n : ℕ in Filter.atTop, ∀ F : Finset (Finset (Fin n)),
    (∀ A ∈ F, A.card = k) → (n - 2).choose (k - 2) < F.card →
      ∃ A ∈ F, ∃ B ∈ F, (A ∩ B).card = 1

Used by 1

Used byFrankl's theorem on families with no singleton intersection

TheoremFrankl's theorem on families with no singleton intersection#●ready to prove

For every \(k \ge 4\) and every sufficiently large \(n\) (depending on \(k\)), every family of more than \(\binom{n-2}{k-2}\) subsets of \(\{1, \dots, n\}\), each with exactly \(k\) elements, contains two sets \(A\) and \(B\) with \(|A \cap B| = 1\).

This resolves Erdős Problem 702 of Erdős and Sós; Katona had the case \(k = 4\). The hypothesis that \(n\) is large is needed (\(k = 4\), \(n = 5\)).

public theorem_wanted noSingletonIntersectionBound_holds : noSingletonIntersectionBound

Sources

• T. F. Bloom, Erdős Problems, Problem #702, https://www.erdosproblems.com/702 (status PROVED); resolution: P. Frankl, On families of finite sets no two of which intersect in a singleton, Bull. Austral. Math. Soc. 17 (1977), 125-134, P. Keevash, D. Mubayi and R. M. Wilson, Set systems with no singleton intersection, abstract: 'Frankl showed that |F| ≤ C(n-2, k-2) for k ≥ 4 and n sufficiently large, confirming a conjecture of Erdős and Sós'; erdosproblems.com/702: Frankl proved this for all k ≥ 4, https://www.math.cmu.edu/users/mubayi/papers/no-singleton.pdf.

Uses 1

Statement usesErdős Problem 702 on singleton intersections

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.