LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-07-31

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A maximal pairwise disjoint subfamily either supplies a sunflower or gives a small transversal for the whole uniform family

Statement

Let $k \geq 1$ , let $F$ be a finite family of distinct $k$ -element sets, and let $r \geq 2$ . If $G \subseteq F$ is maximal among pairwise disjoint subfamilies, then either $∣ G ∣ \geq r$ , in which case $F$ contains an $r$ -petal sunflower with empty core, or

$X : = ⋃_{G \in G} G$

meets every member of $F$ and has cardinality at most $k (r - 1)$ .

Facts & Assumptions

Given: A natural $k \geq 1$ , a finite family $F$ of distinct $k$ -sets, a natural $r \geq 2$ , and a maximal pairwise disjoint subfamily $G$ .

[F1]

Pairwise disjoint distinct sets form a sunflower with empty core (Sunflowers, petals, and their common core).

[F2]

Subsets of finite sets are finite, and a finite disjoint union has cardinality equal to the sum of the cardinalities of its members (The cardinality $∣ A ∣$ of a finite set, A subset of a finite set is finite, with $∣ B ∣ \leq ∣ A ∣$ , and equality holds if and only if $B = A$ , The sum rule: a finite disjoint union is finite with $∣ A \cup B ∣ = ∣ A ∣ + ∣ B ∣$ and $∣ ⋃_{i \in I} A_{i} ∣ = \sum_{i \in I} ∣ A_{i} ∣$ , and a sum over a finite index set splits along a partition).

Proof

technique · direct

1.1

If $∣ G ∣ \geq r$ , any $r$ members of $G$ are pairwise disjoint and therefore form an $r$ -petal sunflower with empty core.

givenF1

1.2

Suppose $∣ G ∣ \leq r - 1$ and put $X = ⋃_{G \in G} G$ . Since the members of $G$ are disjoint $k$ -sets, $∣ X ∣ = k ∣ G ∣ \leq k (r - 1)$ .

givenF2

2.1

Every $F \in F$ meets $X$ . Otherwise $F$ would be disjoint from every $G \in G$ , so $G \cup {F}$ would be a larger pairwise disjoint subfamily, contradicting maximality.

step 1.2given

3.1

Thus the first case gives an empty-core sunflower, while the second gives a transversal $X$ of size at most $k (r - 1)$ meeting every member of $F$ .

step 1.1step 1.2step 2.1∎

Depends on

Used by

Erdős-Rado sunflower lemma: more than k!(r-1)ᵏ distinct k-sets contain an r-petal sunflower Theorem

Dependency tree · two levels

24 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Sunflower (mathematics) (Wikipedia) (standard reference, not scraped)