angle₁₃₂_eq_zero — Mathlib

English

Let p1, p2, p3 be points in a Euclidean affine space. If p2 lies strictly between p1 and p3, then the angle at p3 formed by p1–p3–p2 is zero; i.e. ∠ p1 p3 p2 = 0.

Русский

Пусть p1, p2, p3 — точки в евклидовом аффинном пространстве. Если p2 лежит строго между p1 и p3, то угол ∠ p1 p3 p2 равен 0; то есть точки p1, p3, p2 образуют нулевой угол.

LaTeX

$$$$ \forall p_1,p_2,p_3,\; \operatorname{Between}(p_1,p_2,p_3) \Rightarrow \angle p_1 p_3 p_2 = 0. $$$$

Lean4

/-- If the second of three points is strictly between the other two, the angle at the third point
(reversed) is zero. -/
theorem _root_.Sbtw.angle₁₃₂_eq_zero {p₁ p₂ p₃ : P} (h : Sbtw ℝ p₁ p₂ p₃) : ∠ p₁ p₃ p₂ = 0 :=
  h.wbtw.angle₁₃₂_eq_zero_of_ne h.ne_right

Похожие утверждения