Erdős Problem 224

References:

• erdosproblems.com/224
• [DaGr62] Danzer, L. and Gr"{u}nbaum, B., "{U}ber zwei Probleme bez"{u}glich konvexer K"{o}rper von P. Erd\H{o}s und von V. L. Klee. Math. Z. (1962), 95-99.

def Erdos224.ObtuseAt {d : ℕ} (x y z : EuclideanSpace ℝ (Fin d)) : Prop

The angle $yxz$ is obtuse.

Equations

• Erdos224.ObtuseAt x y z = (inner ℝ (y - x) (z - x) < 0)

theorem Erdos224.erdos_224 {d : ℕ} (A : Finset (EuclideanSpace ℝ (Fin d))) (hcard : A.card = 2 ^ d + 1) : ∃ (x : EuclideanSpace ℝ (Fin d)) (y : EuclideanSpace ℝ (Fin d)) (z : EuclideanSpace ℝ (Fin d)), x ∈ A ∧ y ∈ A ∧ z ∈ A ∧ x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ ObtuseAt x y z

If $A\subseteq \mathbb{R}^d$ is any set of $2^d+1$ points then some three points in $A$ determine an obtuse angle.

The general case was proved by Danzer and Gr"{u}nbaum [DaGr62].