def OrdinalCardinalRamsey (α β : Ordinal.{u}) (c : Cardinal.{u}) : Prop

This proposition asserts the ordinal Ramsey property α → (β, c)².

It states that for any 2-coloring of the complete graph on the ordinal α, one of the following must hold:

• There is a red clique which is order-isomorphic to β.
• There is a blue clique of cardinality c.

Equations

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