Skip to content

Erdős problem 1128

Start work

Erdős Problem 1128 (disproved by Prikry–Mills, 1978):

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/1128.lean

Formal Conjectures

FormalConjectures/ErdosProblems/1128.leanErdos1128.erdos_112810 linesExact file
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

Continue

Start a contributionBrowse the source filesOpen the collection entry