Hinge theorem

TheoremHinge theorem in inner product spaces#✓fully proved

Let \(V\) be a real inner product space and let \(A, B, C, D, E, F \in V\). If \(\|B - A\| = \|E - D\|\), \(\|C - A\| = \|F - D\|\) and \(\langle B - A, C - A \rangle < \langle E - D, F - D \rangle\), then \(\|F - E\| < \|C - B\|\).

Proof: Expand both squared opposite sides by the law of cosines and compare them.

theorem hinge_theorem_of_inner_lt {V : Type*} [NormedAddCommGroup V]
    [InnerProductSpace ℝ V] (A B C D E F : V)
    (hAB : ‖B - A‖ = ‖E - D‖) (hAC : ‖C - A‖ = ‖F - D‖)
    (hinner : inner ℝ (B - A) (C - A) < inner ℝ (E - D) (F - D)) :
    ‖F - E‖ < ‖C - B‖

Sources

• Euclid's Elements, Book I, Proposition 24.

Used by 1

Used byHinge theorem

TheoremHinge theorem#✓fully proved

Let \(A, B, C\) and \(D, E, F\) be two triples of pairwise distinct points of the Euclidean plane \(\mathbb{R}^2\) forming nondegenerate triangles: \(C - A\) is not a real multiple of \(B - A\), and \(F - D\) is not a real multiple of \(E - D\). Write \(XY\) for the distance between points \(X\) and \(Y\). If \(AB = DE\), \(AC = DF\) and \(\langle B - A, C - A \rangle < \langle E - D, F - D \rangle\), that is, the angle at \(A\) is larger than the angle at \(D\), then \(EF < BC\).

Proof: The vector law of cosines compares the squared opposite sides, following Euclid's Elements, Book I, Proposition 24.

theorem hinge_theorem : ∀ (A B C D E F : EuclideanSpace ℝ (Fin 2)),
  B ≠ A → C ≠ A → C ≠ B → E ≠ D → F ≠ D → F ≠ E →
  (∀ t : ℝ, C - A ≠ t • (B - A)) →
  (∀ s : ℝ, F - D ≠ s • (E - D)) →
  ‖B - A‖ = ‖E - D‖ → ‖C - A‖ = ‖F - D‖ →
  inner ℝ (B - A) (C - A) < inner ℝ (E - D) (F - D) →
  ‖F - E‖ < ‖C - B‖

Sources

• Euclid's Elements, Book I, Proposition 24 (https://mathcs.clarku.edu/~djoyce/elements/bookI/propI24.html); see also https://en.wikipedia.org/wiki/Hinge_theorem.

Uses 1

Proof usesHinge theorem in inner product spaces

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.