Documentation

FormalConjectures.ForMathlib.SetTheory.Cardinal.SimpleGraph

This proposition asserts the Ramsey property κ → (κ, c)₂, where κ is the cardinality of the ordinal ω ^ β and c is some cardinal.

It states that for any 2-coloring of the edges of a complete graph on κ vertices, there must be a monochromatic red clique of size κ or a monochromatic blue clique of size c.

Equations
  • One or more equations did not get rendered due to their size.
Instances For