Erdős problem 352

Is there some $c > 0$ such that every measurable $A \subseteq \mathbb{R}^2$ of measure $\geq c$ contains the vertices of a triangle of area 1?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

352.lean

Retained formal statement1 of 1

Is there some $c > 0$ such that every measurable $A \subseteq \mathbb{R}^2$ of measure $\geq c$ contains the vertices of a triangle of area 1?

FormalConjectures/ErdosProblems/352.leanErdos352.erdos_3527 linesExact file

1True ↔2  ∃ c > 0,3    ∀ (A : Set (EuclideanSpace ℝ (Fin 2))),4      MeasurableSet A →5        ↑(MeasureTheory.volume A) ≥ ↑c →6          ∃ t,7            (∀ (p : Fin 3), t.points p ∈ A) ∧ EuclideanGeometry.triangle_area (t.points 0) (t.points 1) (t.points 2) = 1

OpenStatement only, no proof