Pompeiu's theorem

TheoremPompeiu's theorem#✓fully proved

Write \(XY\) for the Euclidean distance between points \(X\) and \(Y\) of the Euclidean plane \(\mathbb{R}^2\). Let \(A\), \(B\), \(C\) be points of the plane with \(AB = BC = CA\) and \(AB > 0\), so that \(ABC\) is an equilateral triangle, and let \(P\) be any point of the plane. Then \(PA \le PB + PC\), \(PB \le PC + PA\) and \(PC \le PA + PB\); that is, \(PA\), \(PB\), \(PC\) are the side lengths of a (possibly degenerate) triangle.

theorem pompeiu_general (A B C P : EuclideanSpace ℝ (Fin 2))
    (h_equilateral : dist A B = dist B C ∧ dist B C = dist C A)
    (h_side_pos : 0 < dist A B) :
    dist P A ≤ dist P B + dist P C ∧
      dist P B ≤ dist P C + dist P A ∧
      dist P C ≤ dist P A + dist P B

Used by 1

Used byPompeiu's theorem for a point other than a vertex

TheoremPompeiu's theorem for a point other than a vertex#✓fully proved

Write \(XY\) for the Euclidean distance between points \(X\) and \(Y\) of the Euclidean plane \(\mathbb{R}^2\). Let \(A\), \(B\), \(C\) be points of the plane with \(AB = BC = CA\) and \(AB > 0\), so that \(ABC\) is an equilateral triangle, and let \(P\) be a point of the plane with \(P \ne A\), \(P \ne B\) and \(P \ne C\). Then \(PA \le PB + PC\), \(PB \le PC + PA\) and \(PC \le PA + PB\); that is, \(PA\), \(PB\), \(PC\) are the side lengths of a (possibly degenerate) triangle.

The hypothesis that \(P\) is not a vertex is not needed: the conclusion holds for every point \(P\) of the plane.

theorem pompeiu (A B C P : EuclideanSpace ℝ (Fin 2))
    (h_equilateral : dist A B = dist B C ∧ dist B C = dist C A)
    (h_side_pos : 0 < dist A B)
    (hP : P ≠ A ∧ P ≠ B ∧ P ≠ C) :
    dist P A ≤ dist P B + dist P C ∧
      dist P B ≤ dist P C + dist P A ∧
      dist P C ≤ dist P A + dist P B

Sources

• https://en.wikipedia.org/wiki/Pompeiu%27s_theorem.

Uses 1

Proof usesPompeiu's theorem

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.