Erdős Problem 1167
Infinite-target case.* When all are infinite and bounded by , , so the hypothesis simplifies to a "pure" stepping-down lemma: $$2^\lambda \to (\kappa_\alpha)_{\alpha<\gamma}^{r+1} ...
Mathematical statement
Infinite-target case.* When all are infinite and bounded by , , so the hypothesis simplifies to a "pure" stepping-down lemma:
\lambda \to (\kappa_\alpha)_{\alpha<\gamma}^r.$$ The condition $\kappa_\alpha \leq \lambda$ is needed to avoid a size obstruction: without it, the conclusion would require a subset of $\lambda$ of size $\kappa_\alpha > \lambda$, which is impossible (see `infinite_targets_needs_bound`).Statement source: Erdős Problems statement material
Statement terms: Source-specific
Source-specific terms. Therefore does not assert reuse rights beyond attributed display.
Statement artifacts, not proofs
These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.
Pinned Lean formulation 1
infinite_targets
theorem infinite_targets (r : ℕ) (hr : 2 ≤ r) (lam : Cardinal.{u}) (hlam : ℵ₀ ≤ lam) (γ : Ordinal.{u}) (hγ : 2 ≤ γ) (κ : γ.ToType → Cardinal.{u}) (hκ : ∀ i, ℵ₀ ≤ κ i) (hκ_le : ∀ i, κ i ≤ lam) : cardinalPartitionRel ((2 : Cardinal.{u}) ^ lam) (r + 1) γ κ → cardinalPartitionRel lam r γ κ := by sorry- Statement source
- Formal Conjectures
- Lean version
- v4.27.0
- Placeholder
- Present; no proof artifact
- Source evidence
- Pinned source index
- Fidelity review
- Community formulation
References