oangle_midpoint_left — Mathlib

English

The same invariance as oangle_midpoint_left holds; the midpoint replacement on the left leaves the oriented angle unchanged.

Русский

Сохраняется аналогичная тождественность при замещении левой точки серединой отрезка.

LaTeX

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

Lean4

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

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