Is the infinitary Ramsey theorem in mathlib?

Stream: new members

[Ching-Tsun Chou]

I mean theorems like this one:

https://en.wikipedia.org/wiki/Ramsey%27s_theorem#Infinite_graphs

[Ching-Tsun Chou]

In fact, I need only the n = 1 case for now. Later I may need the n = 2 case.

[Matt Diamond]

#12773 is infinite Ramsey for hypergraphs

[Matt Diamond]

seems like it stalled last year though

[Matt Diamond]

@Peter Nelson

[Peter Nelson]

I can try dusting it off.

[Peter Nelson]

It was all typechecking at the time.

[Matt Diamond]

the n = 1 case should be easy to prove if we don't already have it

[Matt Diamond]

relevant: docs#Cardinal.infinite_pigeonhole

[Ching-Tsun Chou]

Thanks for the pointers!