Erdős problem 328
Suppose and is such that for all . Can be partitioned into many subsets (where depends only on ) such that for all and ?
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/328.leanFalse ↔ ∀ (C : ℕ), 0 < C → ∃ t, ∀ (A : Set ℕ), (∀ (n : ℕ), AdditiveCombinatorics.sumRep A n ≤ C) → ∃ P, ⋃ i, P i = A ∧ Set.univ.PairwiseDisjoint P ∧ ∀ (i : Fin t) (n : ℕ), AdditiveCombinatorics.sumRep (P i) n < CProof manifests naming this Problem
- Jayyhk Erdős Lean
jayyhk:erdos:328
Reported activity
Work these sources record against this Problem. Source-reported attribution, not reviewed here.
Formalization
- Machine