Zulip Chat Archive

Stream: maths

Topic: Pigeonhole for arbitrary cardinals?


view this post on Zulip Ryan Lahfa (Mar 23 2020 at 19:48):

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 (?).

view this post on Zulip Bhavik Mehta (Mar 23 2020 at 19:51):

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

view this post on Zulip Ryan Lahfa (Mar 23 2020 at 19:54):

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.

view this post on Zulip Ryan Lahfa (Mar 23 2020 at 19:54):

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

view this post on Zulip Bhavik Mehta (Mar 23 2020 at 19:56):

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

view this post on Zulip Bhavik Mehta (Mar 23 2020 at 19:56):

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!

view this post on Zulip Anton Lorenzen (Mar 23 2020 at 19:57):

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

view this post on Zulip Anton Lorenzen (Mar 23 2020 at 19:58):

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

view this post on Zulip Ryan Lahfa (Mar 23 2020 at 20:01):

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


Last updated: May 10 2021 at 07:15 UTC