Sunflower

IsSunflowerdef

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

Used by

Problem CB-002 — the sunflower conjecture

From Mathlib

Data.Finset.Lattice.Basic

import Conjectura.Defs.Mathematics.Combinatorics.Sunflower · maintainer — open · raw source

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

Full credits