angle_comm — Mathlib

English

The angle at a point does not depend on the order of the other two points: ∠p1 p2 p3 = ∠p3 p2 p1.

Русский

Угол в точке не зависит от порядка двух остальных точек: ∠p1 p2 p3 = ∠p3 p2 p1.

LaTeX

$$$\angle p_1 p_2 p_3 = \angle p_3 p_2 p_1$$$

Lean4

/-- The angle at a point does not depend on the order of the other two
points. -/
nonrec theorem angle_comm (p₁ p₂ p₃ : P) : ∠ p₁ p₂ p₃ = ∠ p₃ p₂ p₁ :=
  angle_comm _ _

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