Erdős problem 353
Let be a measurable set with infinite measure. Must contain the vertices of an isosceles trapezoid of area ? What about an isosceles triangle, or a right-angled triangle, or a cyclic quadrilateral, or a convex polygon with congruent sides?
Sources
FormalConjectures/ErdosProblems/
353.lean
Let be a measurable set with infinite measure. Must contain the vertices of an isosceles trapezoid of area ? What about an isosceles triangle, or a right-angled triangle, or a cyclic quadrilateral, or a convex polygon with congruent sides?
Koizumi [Ko25] has resolved this question, proving that any set with infinite measure must contain the vertices of an isosceles trapezoid, an isosceles triangle, and a right-angled triangle, all of area .
This statement formalizes the leading question, for isosceles trapezoids; the remaining configurations are given as variants below. The area of a polygon is taken to be the Lebesgue measure of the convex hull of its vertices.
True ↔ ∀ (A : Set (EuclideanSpace ℝ (Fin 2))), MeasurableSet A → MeasureTheory.volume A = ⊤ → ∃ a ∈ A, ∃ b ∈ A, ∃ c ∈ A, ∃ d ∈ A, EuclideanGeometry.IsIsoscelesTrapezoid a b c d ∧ MeasureTheory.volume ((convexHull ℝ) {a, b, c, d}) = 1