oangle_eq_right — Mathlib

English

Replacing the first point by one on the same line but the opposite ray adds π to the oriented angle: ∡ p1 p2 p3 = ∡ p1' p2 p3 + π.

Русский

Замена первой точки на точку на противоположном луче добавляет π к ориентированному углу: ∡ p1 p2 p3 = ∡ p1' p2 p3 + π.

LaTeX

$$$Sbtw_\mathbb{R}(p_1,p_2,p_1') \Rightarrow \angle p_1 p_2 p_3 = \angle p_1' p_2 p_3 + \pi$$$

Lean4

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

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