Stream: General

Topic: Generalized Pigeonhole Principle


view this post on Zulip Bernhard Pöttinger (May 12 2020 at 08:38):

Hi everyone, is there already a formalization of the generalized pigeonhole principle (k holes, n pigeons, then there is at least one hole with ceil(n/k) pigeons)? I only found the simple one and one for infinite n.

view this post on Zulip Kevin Kappelmann (May 12 2020 at 09:59):

I at least also couldn't find it when searching for pigeonhole. Maybe you are more lucky when fuzzy searching for a specific term and using the filters to narrow down the results. If it's not there, it surely would be a great addition to the library once you proved it :)

view this post on Zulip Manuel Eberl (May 12 2020 at 16:32):

Oops, Max told me to look into this and I proved it.

view this post on Zulip Manuel Eberl (May 12 2020 at 16:33):

But in any case, it's probably good if you can focus on your thesis instead of proving silly little lemmas that ought to be in the library like this one, so no harm done.

view this post on Zulip Manuel Eberl (May 12 2020 at 16:34):

http://downthetypehole.de/paste/l9UcGFqv

view this post on Zulip Manuel Eberl (May 12 2020 at 16:34):

Feel free to copy-paste this into your development for now; I will add it to the library for the next release (unless I forget). Maybe add a small comment that you got it from me.

view this post on Zulip Bernhard Pöttinger (May 13 2020 at 19:22):

@Manuel Eberl Thanks for proving it. I already proved my own variant yesterday and wanted to clean it up now... But yours is more elegant.

view this post on Zulip Manuel Eberl (May 14 2020 at 10:08):

I know added it to the library for the next release, albeit in an equivalent version that doesn't mention rounding or real numbers.


Last updated: Aug 15 2022 at 02:13 UTC