Ramsey-type properties of graph pairs

The Erdős–Hajnal "exceptional pair" trio of predicates:

• HasFiniteRamseyProperty G₁ G₂ — for every n ≥ 1 there is a G₁-free graph H such that every n-edge-colouring of H contains a monochromatic G₂.
• HasCountableRamseyEscape G₁ G₂ — every G₁-free graph H admits a countable edge-colouring with every colour class G₂-free.
• IsErdosHajnalExceptional G₁ G₂ — the conjunction of both.

These were introduced for Erdős Problem 596 but are reusable for Problem 595 and other Ramsey-type questions; we factor them out per mo271's review.

def SimpleGraph.HasFiniteRamseyProperty {U₁ : Type u_1} {U₂ : Type u_2} (G₁ : SimpleGraph U₁) (G₂ : SimpleGraph U₂) : Prop

The finite Ramsey property for the pair $(G_1, G_2)$: for every $n \geq 1$, there exists a $G_1$-free graph H on some vertex type in Type (universe 0) such that every n-edge-colouring of H contains a monochromatic copy of G_2.

Equations

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

def SimpleGraph.HasCountableRamseyEscape {U₁ : Type u_1} {U₂ : Type u_2} (G₁ : SimpleGraph U₁) (G₂ : SimpleGraph U₂) : Prop

The countable Ramsey escape property for the pair $(G_1, G_2)$: every $G_1$-free graph H on a Type-valued vertex type has a countable edge-colouring in which every colour class is $G_2$-free.

Equations

• G₁.HasCountableRamseyEscape G₂ = ∀ (W : Type) (H : SimpleGraph W), G₁.Free H → ∃ (d : ℕ → SimpleGraph W), H.IsEdgeColouring d ∧ ∀ (j : ℕ), G₂.Free (d j)

def SimpleGraph.IsErdosHajnalExceptional {U₁ : Type u_1} {U₂ : Type u_2} (G₁ : SimpleGraph U₁) (G₂ : SimpleGraph U₂) : Prop

A pair $(G_1, G_2)$ is Erdős–Hajnal exceptional if it has both the finite Ramsey property and the countable Ramsey escape property.

Equations

• G₁.IsErdosHajnalExceptional G₂ = (G₁.HasFiniteRamseyProperty G₂ ∧ G₁.HasCountableRamseyEscape G₂)