angle_neg — Mathlib

English

For any vectors v1, v2, v3, negating all three does not change the angle: ∠(−v1) (−v2) (−v3) = ∠v1 v2 v3.

Русский

Для любых векторов v1, v2, v3 угол, образованный векторами −v1, −v2, −v3, равен углу, образованному v1, v2, v3.

LaTeX

$$$\angle(-v_1) (-v_2) (-v_3) = \angle v_1 v_2 v_3$$$

Lean4

/-- Angles in a vector space are invariant to inversion -/
@[simp]
theorem angle_neg (v₁ v₂ v₃ : V) : ∠ (-v₁) (-v₂) (-v₃) = ∠ v₁ v₂ v₃ := by
  simpa only [zero_sub] using angle_const_sub 0 v₁ v₂ v₃

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