oangle_eq_left — Mathlib

English

If p2, p1, p1' lie in weak betweenness and p1' is not equal to p2, then ∡ p1 p2 p3 = ∡ p1' p2 p3.

Русский

Если p2 является между p1 и p1' в слабом смысле и p1' ≠ p2, то ∡ p1 p2 p3 = ∡ p1' p2 p3.

LaTeX

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

Lean4

/-- An oriented angle is unchanged by replacing the first point by one strictly further away on
the same ray. -/
theorem _root_.Sbtw.oangle_eq_left {p₁ p₁' p₂ p₃ : P} (h : Sbtw ℝ p₂ p₁ p₁') : ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃ :=
  h.wbtw.oangle_eq_left h.ne_left

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