Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: The Sunflower Lemma of Erdős a...

view this post on Zulip Email Gateway (Mar 01 2021 at 12:37):

From: Tobias Nipkow <>
The Sunflower Lemma of Erdős and Rado
René Thiemann

We formally define sunflowers and provide a formalization of the sunflower lemma
of Erdős and Rado: whenever a set of size-k-sets has a larger cardinality than
(r - 1)^k · k!, then it contains a sunflower of cardinality r.


Last updated: Dec 08 2021 at 09:20 UTC