Cardinal partition relation

This file defines Combinatorics.cardinalPartitionRel, the multicolor $r$-uniform partition arrow

$$\mu \to (\nu_\alpha)_{\alpha < \gamma}^r$$

between an infinite "source" cardinal $\mu$, a uniformity $r$, an ordinal-indexed family of "target" cardinals $\nu_\alpha$, and a coloring of $r$-element subsets. This is the standard notation in infinitary combinatorics and is reused by several Erdős–Rado-style problems.

def Combinatorics.cardinalPartitionRel (μ : Cardinal.{u}) (r : ℕ) (γ : Ordinal.{u}) (ν : γ.ToType → Cardinal.{u}) : Prop

cardinalPartitionRel μ r γ ν asserts the multicolor $r$-uniform partition relation $$\mu \to (\nu_\alpha)_{\alpha < \gamma}^r.$$

It states: for every type A with #A = μ and every coloring col of the $r$-element finite subsets of A by γ.ToType (the colors indexed by ordinals less than γ), there exists a color i : γ.ToType and a homogeneous subset H : Set A with #H = ν i such that every $r$-element subset of H receives color i.

When γ = 2 and r = 2 this reduces to the classical binary partition relation $\mu \to (\nu_0, \nu_1)^2$.

Equations

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