Pigeonhole for arbitrary cardinals?

Stream: maths

[Ryan Lahfa]

I wanted to understand if it was a misunderstanding on my part, but we don't have any "general" pigeonhole principles in mathlib?

Let's say I have $f : A \to B$ where range f: set B is finite, i.e. I have a proof of (range f).finite and let's say (set A).univ.infinite (something like this), do I have a pigeonhole which gives me something like: there is some y in B such that (preimage f y).infinite (?).

[Bhavik Mehta]

I haven't seen anything like that in mathlib. I have proved something very similar to what you suggest here though: https://github.com/b-mehta/combinatorics/blob/extras/src/inf_ramsey.lean#L10

[Ryan Lahfa]

Bhavik Mehta said:

I haven't seen anything like that in mathlib. I have proved something very similar to what you suggest here though: https://github.com/b-mehta/combinatorics/blob/extras/src/inf_ramsey.lean#L10

Wow, awesome! I didn't know about bind and was using univ.

I guess that's something really fundamental & basic. That would make sense to PR it to mathlib in set I think.

[Ryan Lahfa]

(also would be nice to make it work with finset)

[Bhavik Mehta]

Ryan Lahfa said:

(also would be nice to make it work with finset)

https://github.com/b-mehta/combinatorics/blob/extras/src/ramsey.lean#L11

[Bhavik Mehta]

Ryan Lahfa said:

I guess that's something really fundamental & basic. That would make sense to PR it to mathlib in set I think.

Yeah it would, I just haven't gotten round to it yet. Feel free to do it yourself if you'd like!

[Anton Lorenzen]

I wrote a pigeonhole principle for finset in https://github.com/anfelor/coc-lean/blob/master/src/FreshNames.lean

[Anton Lorenzen]

But there might be nicer approaches; it feels a bit hacked together

[Ryan Lahfa]

Maybe we should wait some inputs from maintainers of mathlib to have their opinion and see what I can collect to do a nice PR :)