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
** case.** The stepping-down from 3-uniform to 2-uniform partition relations: implies . Generalises the classical Erdős–Rado stepping-up/down theorem for pairs.
∀ (lam : Cardinal.{u}), Cardinal.aleph0 ≤ lam → ∀ (γ : Ordinal.{u}), 2 ≤ γ → ∀ (κ : γ.ToType → Cardinal.{u}), (Combinatorics.cardinalPartitionRel (2 ^ lam) 3 γ fun α => κ α + 1) → Combinatorics.cardinalPartitionRel lam 2 γ κOpenStatement only, no proof