IsSunflower
A 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 members of F have intersection exactly C.
Statement
def IsSunflower {α : Type*} [DecidableEq α] (F : Finset (Finset α)) (C : Finset α) : Prop
- Source
- Erdős & Rado, Intersection theorems for systems of sets, J. London Math. Soc. 35 (1960), 85-90 (sunflowers / delta-systems); the concept is absent from Mathlib (`mathlib_grep` for 'sunflower' finds nothing).
- Verified
- 10 Sep 2026
- Axioms
- none listed
- Used by 4
- isSunflower_empty_core_iff_pairwise_disjointA finite family F of finite sets is a sunflower with empty kernel if and only if its members are pairwise disjoint.
- isSunflower_core_uniqueIf a finite family F of finite sets has at least two members and is a sunflower with kernel C and also a sunflower with kernel C', then C…
- isSunflower_monoA subfamily of a sunflower is again a sunflower with the same kernel: if G ⊆ F and F is a sunflower with kernel C, then every member of G…
- exists_family_card_six_no_three_petal_sunflowerThere is a finite family F of six 2-element subsets of a 6-element ground set (namely the six edges of two disjoint triangles) such that…
Read back from the Lean
Given a type α with decidable equality, a finite family F of finite subsets of α, and a finite subset C of α, IsSunflower F C asserts the conjunction of two things:
1. Every member A of F contains C: for all A ∈ F, C ⊆ A (i.e. every element of C lies in A).
2. Any two distinct members of F have intersection exactly C: for all A ∈ F and all B ∈ F, if A ≠ B then A ∩ B = C.
The parameters are in the order (F, C), so C is presented as the candidate "kernel"/"core". DecidableEq α is a typeclass hypothesis restricting α to types with decidable equality (needed for Finset intersection). There is no hypothesis that C ∈ F, that F is nonempty, or that F has at least two members.
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 finite family of finite sets is a sunflower with kernel `C` if all members contain `C` and distinct members meet exactly in `C`. -/ def IsSunflower {α : Type*} [DecidableEq α] (F : Finset (Finset α)) (C : Finset α) : Prop := (∀ A ∈ F, C ⊆ A) ∧ ∀ A ∈ F, ∀ B ∈ F, A ≠ B → A ∩ B = C