Add Pigeon Hole principle.
All threads resolved!
All threads resolved!
I was surprised that we do not have the Pigeon hole principle. It's a trivial consequence of results we already have on Finite types and cardinalities.
Merge request reports
Activity
Filter activity
I don't think
fin
makes sense, since the lemma is about any finite type, not about thefin
type (which is a very specific finite type).We could add
finite
, but I am not sure that makes sense since the non-finite Pigeon hole principle is non-standard. Or would you say that the Pigeon Hole principle is a specific property on functions on nat (with a bound), instead of a general property of finite types?- Resolved by Robbert Krebbers
enabled an automatic merge when the pipeline for 6f9dea44 succeeds
mentioned in commit 4fb85912
Please register or sign in to reply