Documentation

FormalConjectures.ErdosProblems.«352»

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?