isSunflower_empty_core_iff_pairwise_disjoint
A finite family F of finite sets is a sunflower with empty kernel if and only if its members are pairwise disjoint.
Statement
theorem isSunflower_empty_core_iff_pairwise_disjoint {α : Type*} [DecidableEq α] (F : Finset (Finset α)) : IsSunflower F ∅ ↔ ∀ A ∈ F, ∀ B ∈ F, A ≠ B → Disjoint A B
- Source
- Folklore sanity lemma for the sunflower kernel; it supplies the base case of the Erdős-Rado sunflower lemma `exists_isSunflower_of_card_gt_factorial_mul`. Disjointness form: `Finset.disjoint_iff_inter_eq_empty` (Mathlib).
- Verified
- 10 Sep 2026
- Axioms
Classical.choiceQuot.soundpropext- Built on 1
- IsSunflowerA finite family F of finite sets is a sunflower (a delta-system) with kernel C if every member of F contains C and any two distinct…
Read back from the Lean
For every type α with a decidable equality instance, and every finite family F of finite subsets of α, the following two propositions are equivalent:
(1) F is a sunflower with empty core ∅, meaning every member of F contains ∅ and any two distinct members A and B of F have intersection exactly ∅.
(2) F is pairwise disjoint, meaning for all A, B ∈ F with A ≠ B, A and B are disjoint.
The first conjunct of (1), that every A ∈ F contains ∅, is automatically true. Thus the theorem asserts that F has empty core as a sunflower iff its distinct members have pairwise empty intersections. There are no hypothesis-side restrictions beyond the typeclass [DecidableEq α]; the statement is an iff, not an implication.
Written by a model that saw only the Lean, never the English above. If the two disagree, that is worth a challenge.
Lean source view module on GitHub
/-- A family is a sunflower with empty kernel iff its members are pairwise disjoint. -/ theorem isSunflower_empty_core_iff_pairwise_disjoint {α : Type*} [DecidableEq α] (F : Finset (Finset α)) : IsSunflower F ∅ ↔ ∀ A ∈ F, ∀ B ∈ F, A ≠ B → Disjoint A B := by simp [IsSunflower, Finset.disjoint_iff_inter_eq_empty]