oangle_sign_eq_right — Mathlib

English

If p2 p3 p3' are in weak betweenness and p3 ≠ p2, the right-hand angle signs are preserved: (∡ p2 p4 p3).sign = (∡ p1 p4 p3).sign.

Русский

Если p2 p3 p3' лежат на одной прямой и p3 ≠ p2, знаки углов сохраняются после перестановок на правой стороне.

LaTeX

$$$Wbtw_\mathbb{R}(p_2,p_3,p_3') \land p_3 \neq p_2 \Rightarrow \angle p_2 p_4 p_3).sign = (\angle p_1 p_4 p_3).sign$$$

Lean4

/-- Given three points in strict order on the same line, and a fourth point, the angles at the
fourth point between the second and third or first and third points have the same sign. -/
theorem _root_.Sbtw.oangle_sign_eq_right {p₁ p₂ p₃ : P} (p₄ : P) (h : Sbtw ℝ p₁ p₂ p₃) :
    (∡ p₂ p₄ p₃).sign = (∡ p₁ p₄ p₃).sign :=
  h.wbtw.oangle_sign_eq_of_ne_right _ h.ne_right

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