Erdős problem 1128
Erdős Problem 1128 (disproved by Prikry–Mills, 1978):
Sources
FormalConjectures/ErdosProblems/
1128.lean
Retained formal statement
Erdős Problem 1128 (disproved by Prikry–Mills, 1978):
Erdős asked whether every 2-colouring of , where , must contain a monochromatic countable box with .
The answer is No: Prikry and Mills constructed a 2-colouring of with no monochromatic countable box.
Note: The positive statement asserts that every 2-colouring of every contains a monochromatic countably infinite box. Since the answer is False, this positive statement fails.
False ↔ ∀ (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₁SolvedStatement only, no proof