Sunflower

Conjectura.Defs.Mathematics.Combinatorics.Sunflower

/-
Copyright (c) 2026 The Conjectura Authors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: The Conjectura Authors
-/
import Mathlib.Data.Finset.Lattice.Basic

/-! # Sunflower -/

namespace Conjectura.Combinatorics

/-- A **sunflower** is a family of sets any two of which meet in the same common core. The
sunflower lemma, and the conjecture on how few sets force one to appear, are central to
extremal set theory and to circuit lower bounds. -/
def IsSunflower {α : Type*} [DecidableEq α]
    (F : Finset (Finset α)) (core : Finset α) : Prop :=
  ∀ A ∈ F, ∀ B ∈ F, A ≠ B → A ∩ B = core

end Conjectura.Combinatorics