erdos_865.variants.k2

It is a classical folklore fact that if $A\subseteq \{1,\ldots,2N\}$ has size $\geq N+2$ then there are distinct $a,b\in A$ such that $a+b\in A$, which establishes the $k=2$ case.

theorem erdos_865.variants.k2 (N : ℕ) :
    ∀ A ⊆ Icc 1 (2 * N), A.card ≥ N + 2 →
    ∃ a ∈ A, ∃ b ∈ A, a ≠ b ∧ a + b ∈ A

Recent Submissions

No submissions yet. Be the first to attempt this problem.