Bernhard Pöttinger (May 12 2020 at 08:38): 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.
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 :)
Manuel Eberl (May 12 2020 at 16:32):Oops, Max told me to look into this and I proved it.
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.
Manuel Eberl (May 12 2020 at 16:34):http://downthetypehole.de/paste/l9UcGFqv
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.
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.
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: Dec 21 2024 at 16:20 UTC