isSunflower_mono
A 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 contains C and any two distinct members of G intersect in exactly C, so G is a sunflower with kernel C.
Statement
theorem isSunflower_mono {α : Type*} [DecidableEq α] {F G : Finset (Finset α)} {C : Finset α} (hGF : G ⊆ F) (h : IsSunflower F C) : IsSunflower G C
- Source
- folklore; supporting step for exists_isSunflower_of_card_gt_factorial_mul_pow, using the kernel form of the KB definition IsSunflower.
- 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, for all finite sets F and G whose elements are finite subsets of α and every finite subset C of α, in this order of hypotheses: if G ⊆ F (i.e. every member of G is a member of F) and F is a sunflower with center C, then G is a sunflower with center C.
Unfolding the knowledge-base predicate, the hypothesis IsSunflower F C means:
1. for every A ∈ F, C ⊆ A; and
2. for every A ∈ F and every B ∈ F, if A ≠ B then A ∩ B = C.
The conclusion IsSunflower G C means:
1. for every A ∈ G, C ⊆ A; and
2. for every A ∈ G and every B ∈ G, if A ≠ B then A ∩ B = C.
Thus the declaration asserts that the property of being a sunflower with a fixed center C is monotone with respect to taking subfamilies: every subfamily G of a C-centered sunflower F is again a C-centered sunflower.
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 subfamily of a sunflower with kernel C is a sunflower with kernel C. -/ theorem isSunflower_mono {α : Type*} [DecidableEq α] {F G : Finset (Finset α)} {C : Finset α} (hGF : G ⊆ F) (h : IsSunflower F C) : IsSunflower G C := by rw [IsSunflower] at h ⊢ exact ⟨fun A hA => h.1 A (hGF hA), fun A hA B hB hne => h.2 A (hGF hA) B (hGF hB) hne⟩