Erdős problem 881
Let A ⊂ ℕ be an additive basis of order k which is minimal in the sense that if B ⊂ A is any infinite set, then A \ B is not a basis of order k.
Sources
FormalConjectures/ErdosProblems/
881.lean
Retained formal statement
Let A ⊂ ℕ be an additive basis of order k which is minimal in the sense that if B ⊂ A is any infinite set, then A \ B is not a basis of order k.
Must there exist an infinite B ⊂ A such that A \ B is an additive basis of order k + 1?
True ↔ ∀ (k : ℕ) (A : Set ℕ), Erdos881.IsMinimalAsymptoticAddBasisOfOrder k A → ∃ B ⊆ A, B.Infinite ∧ (A \ B).IsAsymptoticAddBasisOfOrder (k + 1)OpenStatement only, no proof