Union-free families

DefinitionFamilies in which no member is a union of other members#✓fully proved

A family \(F\) of finite sets is union-free over its subfamilies if no member \(A \in F\) is the union of a nonempty subfamily of \(F\) that does not contain \(A\).

def SubfamilyUnionFree {α : Type*} [DecidableEq α]
    (F : Finset (Finset α)) : Prop :=
  ∀ A ∈ F, ∀ T ⊆ F.erase A, T.Nonempty → T.sup id ≠ A

DefinitionUnion-free family#✓fully proved

A family \(F\) of subsets of \(\{0, \dots, n-1\}\) is union-free if there are no pairwise distinct \(A, B, C \in F\) with \(A \cup B = C\).

def IsUnionFree {n : ℕ} (F : Finset (Finset (Fin n))) : Prop :=
  ∀ A ∈ F, ∀ B ∈ F, ∀ C ∈ F, A ≠ B → A ≠ C → B ≠ C → A ∪ B ≠ C

Used by 1

Used byMaximum size of a union-free family

DefinitionMaximum size of a union-free family#✓fully proved

For a natural number \(n\), the largest size \(|F|\) of a union-free family \(F\) of subsets of \(\{0, \dots, n-1\}\).

noncomputable def maxUnionFreeSize (n : ℕ) : ℕ :=
  sSup {k : ℕ | ∃ F : Finset (Finset (Fin n)), IsUnionFree F ∧ F.card = k}

Uses 1 · Used by 2

Statement usesUnion-free family

Used byErdős Problem 447, second question · Erdős Problem 447, first question

DefinitionErdős Problem 447, first question#✓fully proved

The assertion that the maximum size of a union-free family of subsets of \(\{0, \dots, n-1\}\) is \(o(2^n)\) as \(n \to \infty\).

def maxUnionFreeSizeLittleO : Prop :=
  (fun n : ℕ => (maxUnionFreeSize n : ℝ)) =o[Filter.atTop] fun n : ℕ => (2 : ℝ) ^ n

Uses 1 · Used by 1

Statement usesMaximum size of a union-free family

Used byUnion-free families have vanishing density (Erdős Problem 447)

DefinitionErdős Problem 447, second question#✓fully proved

The assertion that, for every real \(\varepsilon > 0\) and all sufficiently large \(n\), the maximum size of a union-free family of subsets of \(\{0, \dots, n-1\}\) is at most \((1 + \varepsilon)\binom{n}{\lfloor n/2 \rfloor}\); that is, it is at most \((1 + o(1))\binom{n}{\lfloor n/2 \rfloor}\).

def maxUnionFreeSizeCentralBinomial : Prop :=
  ∀ ε : ℝ, 0 < ε → ∀ᶠ n : ℕ in Filter.atTop,
    (maxUnionFreeSize n : ℝ) ≤ (1 + ε) * n.choose (n / 2)

Uses 1 · Used by 1

Statement usesMaximum size of a union-free family

Used byKleitman's bound for union-free families (Erdős Problem 447)

TheoremUnion-free families have vanishing density (Erdős Problem 447)#●ready to prove

The maximum size of a union-free family of subsets of \(\{0, \dots, n-1\}\) is \(o(2^n)\) as \(n \to \infty\).

This follows from Kleitman's bound \((1 + o(1))\binom{n}{\lfloor n/2 \rfloor}\); Erdős reported an earlier unpublished proof by Sárközy and Szemerédi.

public theorem_wanted maxUnionFreeSizeLittleO_holds : maxUnionFreeSizeLittleO

Sources

• T. F. Bloom, Erdős Problems, Problem #447, https://www.erdosproblems.com/447 (status PROVED (LEAN)); resolution: D. Kleitman, Collections of subsets containing no two sets and their union, Proceedings of the LA Meeting AMS (1971), 153-155, |F| < (1 + o(1)) C(n, ⌊n/2⌋) (erdosproblems.com/447).

Uses 1

Statement usesErdős Problem 447, first question

TheoremKleitman's bound for union-free families (Erdős Problem 447)#●ready to prove

For every real \(\varepsilon > 0\) and all sufficiently large \(n\), the maximum size of a union-free family of subsets of \(\{0, \dots, n-1\}\) is at most \((1 + \varepsilon)\binom{n}{\lfloor n/2 \rfloor}\); that is, it is at most \((1 + o(1))\binom{n}{\lfloor n/2 \rfloor}\).

public theorem_wanted maxUnionFreeSizeCentralBinomial_holds : maxUnionFreeSizeCentralBinomial

Sources

• T. F. Bloom, Erdős Problems, Problem #447, https://www.erdosproblems.com/447 (status PROVED (LEAN)); resolution: D. Kleitman, Collections of subsets containing no two sets and their union, Proceedings of the LA Meeting AMS (1971), 153-155, |F| < (1 + o(1)) C(n, ⌊n/2⌋) (erdosproblems.com/447).

Uses 1

Statement usesErdős Problem 447, second question

5 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.