Erdős problem 1167
Erdős Problem 1167. Let be finite, , and be an infinite cardinal. Let be cardinals for all . Is it true that implies Here means cardinal addition, so that if is infinite.
Sources
FormalConjectures/ErdosProblems/
1167.lean
Retained formal statement
The partition relation with a single color is equivalent to .
∀ (μ : Cardinal.{u}) (r : ℕ) (ν : Ordinal.ToType 1 → Cardinal.{u}), Combinatorics.cardinalPartitionRel μ r 1 ν ↔ μ ≥ ν Erdos1167.i0APIStatement only, no proof