Stream: Mirror: Isabelle Users Mailing List

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

Email Gateway (Mar 01 2021 at 12:37):

From: Tobias Nipkow <nipkow@in.tum.de>
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.

https://www.isa-afp.org/entries/Sunflowers.html

Enjoy!
smime.p7s

Last updated: Jan 04 2025 at 20:18 UTC