An additively closed set containing [a, 2a] contains [a, ∞)

Main results

• ConjeturaC.mem_of_Icc_subset: if S ⊆ ℕ is closed under addition and contains every i with a ≤ i ≤ 2a (a > 0), then it contains every i ≥ a.

theorem ConjeturaC.mem_of_Icc_subset {a : ℕ} (ha : 0 < a) {S : Set ℕ} (hadd : ∀ (x y : ℕ), x ∈ S → y ∈ S → x + y ∈ S) (hI : ∀ (i : ℕ), a ≤ i → i ≤ 2 * a → i ∈ S) (i : ℕ) : a ≤ i → i ∈ S