Erdős Problem 598

Reference: erdosproblems.com/598

noncomputable def Erdos598.κ : Cardinal.{u_2}

Let $\kappa = (2^{\aleph_0})^+$. This is the successor cardinal of the continuum.

Equations

• Erdos598.κ = Order.succ (2 ^ Cardinal.aleph0)

theorem Erdos598.erdos_598 (m : Type u_1) [Infinite m] : (∃ (c : { s : Set m // s.Countable } → Quotient.out κ), ∀ (X : Set m), Cardinal.mk ↑X = κ → c '' {s : { sub : Set m // sub.Countable } | ↑s ⊆ X} = Set.univ) ↔ sorry

Erdős Problem 598: Let $m$ be an infinite cardinal and $\kappa$ be the successor cardinal of $2^{\aleph_0}$. Can one colour the countable subsets of $m$ using $\kappa$ many colours so that every $X \subseteq m$ with $|X| = \kappa$ contains subsets of all possible colours?