Erdős problem 1145 · problems.science

Let $A=\{1\leq a_1 < a_2 < \cdots\}$ and $B=\{1\leq b_1 < b_2 < \cdots\}$ be sets of integers with $a_n/b_n\to 1$ .

Sources

Browse retained paths and inspect the exact material available for this Problem.

2 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

1145.lean

Retained formal statement2 of 2

A stronger form of [erdosproblems.com/28].

FormalConjectures/ErdosProblems/1145.leanErdos1145.erdos_1145.test_implies_erdos_282 linesExact file

1Erdos1145.Erdos1145Prop →2  ∀ (A : Set ℕ), (A + A)ᶜ.Finite → Filter.limsup (fun n => ↑(AdditiveCombinatorics.sumRep A n)) Filter.atTop = ⊤

TestStatement only, no proof