Erdős Problem 352 #
Reference: erdosproblems.com/352
theorem
Erdos352.erdos_352 :
(∃ c > 0,
∀ (A : Set (EuclideanSpace ℝ (Fin 2))),
MeasurableSet A →
↑(MeasureTheory.volume A) ≥ ↑c →
∃ (t : Affine.Triangle ℝ (EuclideanSpace ℝ (Fin 2))),
(∀ (p : Fin 3), t.points p ∈ A) ∧ EuclideanGeometry.triangle_area (t.points 0) (t.points 1) (t.points 2) = 1) ↔ sorry
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?