Erdős problem 120

Let $A \subseteq \mathbb{R}$ be an infinite set. Must there be a set $E \subseteq \mathbb{R}$ of positive measure which does not contain any set of the shape $a * A + b$ for some $a,b \in \mathbb{R}$ and $a \neq 0$ ?

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

120.lean

Retained formal statement1 of 2

Let $A \subseteq \mathbb{R}$ be an infinite set. Must there be a set $E \subseteq \mathbb{R}$ of positive measure which does not contain any set of the shape $a * A + b$ for some $a,b \in \mathbb{R}$ and $a \neq 0$ ?

FormalConjectures/ErdosProblems/120.leanErdos120.erdos_1201 lineExact file

1True ↔ ∀ (A : Set ℝ), A.Infinite → Erdos120.Erdos120For A

OpenStatement only, no proof