Erdős Problem #70

`OrdinalCardinalRamsey3 α β c` asserts the 3-uniform ordinal Ramsey property \(\alpha \to (\beta, c)^3_2\). It states that for any 2-coloring of all 3-element subsets of (the ordinal type) \(\alpha\), one of the following must hold: * There is a red-monochromatic subset of order type \(\beta\): every 3-element sub-subset is colored red. (Formally: a set \(s \subseteq \alpha\) with \(\operatorname{typeLT} s = \beta\) such that any three distinct elements of \(s\) are colored red.) * There is a blue-monochrom

`RealCardinalRamsey3 β c` asserts the 3-uniform partition relation \(\mathfrak{c} \to (\beta, c)^3_2\), where \(\mathfrak{c}\) is the order type of the real numbers with their usual order. It states that for any 2-coloring of all 3-element subsets of \(\mathbb{R}\), one of the following must hold: * There is a red-monochromatic subset of order type \(\beta\): the range of an order embedding `β.ToType ↪o ℝ` such that any three distinct elements of the range are colored red. * There is a blue-monochromati