Erdős Problem 1167

Conjecture 1167 · Erdős

**Finite-target case.** When all $\kappa_\alpha$ are finite, $\kappa_\alpha + 1$ is the ordinary natural-number successor. Special case of erdos_1167.

Formal statement · Lean 4.lean

theorem finite_targets (r : ℕ) (hr : 2 ≤ r) (lam : Cardinal.{u}) (hlam : ℵ₀ ≤ lam)
    (γ : Ordinal.{u}) (hγ : 2 ≤ γ) (n : γ.ToType → ℕ) :
    cardinalPartitionRel ((2 : Cardinal.{u}) ^ lam) (r + 1) γ
        (fun α => (n α : Cardinal.{u}) + 1) →
    cardinalPartitionRel lam r γ (fun α => (n α : Cardinal.{u})) := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗