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.

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 :)

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

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.

http://downthetypehole.de/paste/l9UcGFqv

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.

@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.

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: Dec 07 2023 at 08:19 UTC