Sets meeting but not containing members of a family

DefinitionSets meeting but not containing the members of a family#✓fully proved

For a finite family \(F\) of finite sets of natural numbers with union \(X\), this is the finite set of all \(B \subseteq X\) that meet every member of \(F\) and contain none of them.

def transversalNonCoverSets (F : Finset (Finset ℕ)) : Finset (Finset ℕ) :=
  (F.biUnion id).powerset.filter fun B => ∀ A ∈ F, (A ∩ B).Nonempty ∧ ¬ A ⊆ B

Used by 1

Used byErdős Problem 1027 (sets meeting but not containing members of a family)

DefinitionErdős Problem 1027 (sets meeting but not containing members of a family)#✓fully proved

For every real \(c > 0\) there is a real \(\delta > 0\) such that, for all sufficiently large \(n\), every finite family \(F\) of finite sets of natural numbers, each of size \(n\), with \(|F| \le c \cdot 2^n\) and with union \(X\), has at least \(\delta \cdot 2^{|X|}\) subsets \(B \subseteq X\) that meet every member of \(F\) and contain none of them.

def manyTransversalNonCoverSets : Prop :=
  ∀ c : ℝ, 0 < c → ∃ δ : ℝ, 0 < δ ∧ ∀ᶠ n : ℕ in Filter.atTop, ∀ F : Finset (Finset ℕ),
    (∀ A ∈ F, A.card = n) → (F.card : ℝ) ≤ c * 2 ^ n →
      δ * 2 ^ (F.biUnion id).card ≤ (transversalNonCoverSets F).card

Uses 1 · Used by 1

Statement usesSets meeting but not containing the members of a family

Used byErdős Problem 1027 holds

TheoremErdős Problem 1027 holds#●ready to prove

For every real \(c > 0\) there is a real \(\delta > 0\) such that, for all sufficiently large \(n\), every finite family \(F\) of finite sets of natural numbers, each of size \(n\), with \(|F| \le c \cdot 2^n\) and with union \(X\), has at least \(\delta \cdot 2^{|X|}\) subsets \(B \subseteq X\) that meet every member of \(F\) and contain none of them.

public theorem_wanted manyTransversalNonCoverSets_holds : manyTransversalNonCoverSets

Sources

• T. F. Bloom, Erdős Problems, Problem #1027, https://www.erdosproblems.com/1027 (status PROVED); resolution: K. Chan, proof in the erdosproblems.com/1027 comments; formal proof plby/lean-proofs, erdosproblems.com/1027: 'This is true, and a proof was given in the comment section by Koishi Chan', https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1027.lean#L209.

Uses 1

Statement usesErdős Problem 1027 (sets meeting but not containing members of a family)

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.