oangle_midpoint_rev_left — Mathlib

English

Replacing the third point by the midpoint with the second also preserves the angle: ∡ 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 first point with the midpoint of the segment
between the second point and that point. -/
@[simp]
theorem oangle_midpoint_rev_left (p₁ p₂ p₃ : P) : ∡ (midpoint ℝ p₂ p₁) p₂ p₃ = ∡ p₁ p₂ p₃ := by
  rw [midpoint_comm, oangle_midpoint_left]

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