Erdős problem 352 · problems.science

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

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

1 retained statement2415f78e850a

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

Sources

Search problems.science