isSunflower_core_unique
If 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 = C'.
Statement
theorem isSunflower_core_unique {α : Type*} [DecidableEq α] {F : Finset (Finset α)} {C C' : Finset α} (h : IsSunflower F C) (h' : IsSunflower F C') (hF : 2 ≤ F.card) : C = C'
- Source
- Folklore sanity lemma for the sunflower kernel (the kernel of a sunflower with at least two sets is well defined); needed so that 'the kernel' of a sunflower in `exists_isSunflower_of_card_gt_factorial_mul` is unambiguous.
- 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 any type α (with decidable equality), any finite family F : Finset (Finset α) of finite subsets of α, and any two finite subsets C, C' of α: if C is a sunflower core for F, and C' is a sunflower core for F, and F contains at least 2 members, then C and C' are equal. Spelled out with the definition unfolded in the hypotheses: - h : (∀ A ∈ F, C ⊆ A) ∧ (∀ A ∈ F, ∀ B ∈ F, A ≠ B → A ∩ B = C) - h' : (∀ A ∈ F, C' ⊆ A) ∧ (∀ A ∈ F, ∀ B ∈ F, A ≠ B → A ∩ B = C') - hF : 2 ≤ F.card - conclusion: C = C' So: the "core" of a family with at least two members — the set contained in every member and equal to the intersection of every two distinct members — is unique; any two sets satisfying that property coincide.
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
/-- The kernel of a sunflower with at least two members is unique. -/ theorem isSunflower_core_unique {α : Type*} [DecidableEq α] {F : Finset (Finset α)} {C C' : Finset α} (h : IsSunflower F C) (h' : IsSunflower F C') (hF : 2 ≤ F.card) : C = C' := by have hF' : 1 < F.card := by omega rw [Finset.one_lt_card] at hF' obtain ⟨A, hA, B, hB, hAB⟩ := hF' rw [IsSunflower] at h h' rw [← h.2 A hA B hB hAB, ← h'.2 A hA B hB hAB]