Zulip Chat Archive

Stream: graph theory

Topic: Ramsey THeory

Hunter Monroe (Jul 10 2021 at 04:46):

@Bhavik Mehta would you be willing to update your finite and infinite Ramsey proofs to work with the current mathlib? I tried that with the finite version and fixed a problem exists_mem_of_ne_empty with the finite version (see my fix using calc) but could not work out how to fix insert_empty_eq_singleton. It would be good to get some version of your proofs into mathlib which can later be improved upon and generalized.

Bhavik Mehta (Jul 10 2021 at 18:15):

I can have a go at updating the infinite Ramsey proof, that's pretty much in a maximal generality. For the finite Ramsey proof, I think the approach isn't quite right, and that it would actually be easier to go straight for a more general version

Last updated: Dec 20 2023 at 11:08 UTC