Problem
erdos:1128False ↔ ∀ (A B C : Type), Cardinal.mk A = Cardinal.aleph 1 → Cardinal.mk B = Cardinal.aleph 1 → Cardinal.mk C = Cardinal.aleph 1 → ∀ (f : A → B → C → Fin 2), ∃ A₁ B₁ C₁, Cardinal.mk ↑A₁ = Cardinal.aleph 0 ∧ Cardinal.mk ↑B₁ = Cardinal.aleph 0 ∧ Cardinal.mk ↑C₁ = Cardinal.aleph 0 ∧ Erdos1128.IsMonochromaticBox f A₁ B₁ C₁
Matching claims
No direct claims
This problem has no directly related claim record.