Hypergraph colouring, matchings and covers

Property B and hypergraph colouring, Erdős–Faber–Lovász, Kneser hypergraphs, independence in Steiner and linear triple systems, set mappings, strongly maximal matchings, minimal covers, transversals, Baranyai's theorem and common elements of small set families.

• Erdős–Faber–Lovász conjecture
• Hitting sets for partial designs
• Hypergraph chromatic number
• Degrees in 3-chromatic hypergraphs
• Independence in linear triple systems
• Independent sets in hypergraphs
• Independent sets of set mappings on pairs
• Intersecting families with large cover number
• Kneser hypergraphs
• Sets meeting but not containing members of a family
• Strong matchings and covers in hypergraphs
• Transversal-critical triple systems

TheoremBaranyai's theorem#✓fully proved

Let \(n\) and \(h\) be natural numbers with \(h \mid n\), and let \(V = \{0, \dots, n-1\}\). The \(h\)-element subsets of \(V\), the edges of the complete \(h\)-uniform hypergraph on \(V\), can be partitioned into perfect matchings: there is a finite family \(\mathcal{P}\) of sets of subsets of \(V\) such that the union of the members of \(\mathcal{P}\) is exactly the set of \(h\)-element subsets of \(V\), distinct members of \(\mathcal{P}\) are disjoint, and each member of \(\mathcal{P}\) consists of pairwise disjoint sets whose union is \(V\).

theorem baranyai_theorem : ∀ (n h : ℕ), h ∣ n →
    ∃ P : Finset (Finset (Finset (Fin n))),
      P.biUnion id = Finset.powersetCard h Finset.univ ∧
        (∀ M₁ ∈ P, ∀ M₂ ∈ P, M₁ ≠ M₂ → Disjoint M₁ M₂) ∧
        ∀ M ∈ P, M.biUnion id = Finset.univ ∧
          ∀ e₁ ∈ M, ∀ e₂ ∈ M, e₁ ≠ e₂ → Disjoint e₁ e₂

Sources

• https://en.wikipedia.org/wiki/Baranyai%27s_theorem.

DefinitionProperty B for families of finite sets#✓fully proved

A family F of finite sets has property B (equivalently, it is 2-colourable, i.e. its chromatic number is at most 2) if there is a 2-colouring of the ground set under which no member of F is monochromatic.

def HasPropertyB {α : Type*} (F : Finset (Finset α)) : Prop :=
  ∃ f : α → Fin 2, ∀ A ∈ F, ∃ x ∈ A, ∃ y ∈ A, f x ≠ f y

TheoremScottish Book Problem 9 (a common element of small finite sets)#●ready to prove

Let \(n\) be a natural number, let \(\alpha\) be a nonempty set, and let \((E_i)_{i \in I}\) be a family of finite subsets of \(\alpha\), indexed by an arbitrary set \(I\), with \(|E_i| \le n\) for every \(i \in I\). Suppose that for all indices \(i_0, i_1, \dots, i_n \in I\), not necessarily distinct, the sets \(E_{i_0}, E_{i_1}, \dots, E_{i_n}\) have an element in common. Then some element of \(\alpha\) lies in every \(E_i\).

The hypothesis is read with repetitions allowed: it quantifies over all choices of \(n + 1\) indices, not only over \(n + 1\) distinct members. Under the distinct-members reading the claim would be false when the family has at most \(n\) members (the hypothesis is then vacuous), so the repetition reading is the intended one.

theorem_wanted finiteSetsCommonElement :
    ∀ (n : ℕ) {α : Type} [Nonempty α] (ι : Type) (E : ι → Finset α),
      (∀ i, (E i).card ≤ n) →
      (∀ s : Fin (n + 1) → ι, (⋂ i, (E (s i) : Set α)).Nonempty) →
      (⋂ i, (E i : Set α)).Nonempty

Sources

• S. Mazur and W. Orlicz, Problem 9 of the Scottish Book, stated as a theorem by Ulam in the Scottish Book typescript; see also the 2026 survey "90+ years of the Scottish Book" (arXiv:2603.27867), which records that Ulam solved Problem 9.

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.