oangle_midpoint_right — Mathlib

English

Replacing the first point by the midpoint of p2 and p1 yields the same oriented angle: ∡(midpoint p2 p1) p2 p3 = ∡ p1 p2 p3.

Русский

Замена первой точки на середину p2 p1 даёт тот же угол: ∡(midpoint p2 p1) p2 p3 = ∡ p1 p2 p3.

LaTeX

$$$\angle(\mathrm{midpoint}(p_2,p_1))\; p_2\; p_3 = \angle p_1 p_2 p_3$$$

Lean4

/-- An oriented angle is unchanged by replacing the third point with the midpoint of the segment
between it and the second point. -/
@[simp]
theorem oangle_midpoint_right (p₁ p₂ p₃ : P) : ∡ p₁ p₂ (midpoint ℝ p₃ p₂) = ∡ p₁ p₂ p₃ :=
  by
  by_cases h : p₃ = p₂; · simp [h]
  exact (sbtw_midpoint_of_ne ℝ h).symm.oangle_eq_right

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