Erdős problem 316
Is it true that if is a finite set with then there is a partition such that for ?
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/316.leanFalse ↔ ∀ (A : Finset ℕ), 0 ∉ A → 1 ∉ A → ∑ n ∈ A, 1 / ↑n < 2 → ∃ A₁ A₂, Disjoint A₁ A₂ ∧ A = A₁ ∪ A₂ ∧ ∑ n ∈ A₁, 1 / ↑n < 1 ∧ ∑ n ∈ A₂, 1 / ↑n < 1Proof manifests naming this Problem
- Jayyhk Erdős Lean
jayyhk:erdos:316 - PLBY Lean proofs
ErdosProblems.Erdos316