oangle_midpoint_rev_right — Mathlib

English

Replacing the third point by the midpoint with the second leaves the angle unchanged: ∡ p1 p2 (midpoint p3 p2) = ∡ p1 p2 p3.

Русский

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

LaTeX

$$$\angle p_1 p_2 (\mathrm{midpoint}(p_3,p_2)) = \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 the second point and that point. -/
@[simp]
theorem oangle_midpoint_rev_right (p₁ p₂ p₃ : P) : ∡ p₁ p₂ (midpoint ℝ p₂ p₃) = ∡ p₁ p₂ p₃ := by
  rw [midpoint_comm, oangle_midpoint_right]

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