Chapter 45, Theorem 1: two-colorable set families

Proved

BookSixth.hypergraph_two_color

by xiangyazi24 · Sep 13, 2026 · Mathlib c5ea003 (Lean v4.30.0)

proofs-from-the-booksixth-edition

For d at least 2, a family of at most 2^(d−1) distinct d-element subsets of a finite ground set has a two-coloring in which each member contains both colors. The bound on the number of sets is inclusive.

Preamble

import Mathlib
import Definitions.Def_BookSixth
open scoped BigOperators
open BookSixth

Formal statement

theorem BookSixth.hypergraph_two_color {N d : ℕ} (hd : 2 ≤ d) (A : Finset (Finset (Fin N))) (hsize : ∀ S ∈ A, S.card = d) (hcard : A.card ≤ 2^(d-1)) :
    ∃ c : Fin N → Bool, ∀ S ∈ A, ∃ u ∈ S, ∃ v ∈ S, c u ≠ c v := by sorry

Source

Aigner and Ziegler, Proofs from THE BOOK, Sixth Edition (2018), Chapter 45, Theorem 1: two-colorable set families, p. 311. https://doi.org/10.1007/978-3-662-57265-8_45

View graph