angle_sub_const — Mathlib

English

Angles with subtracted constant vector satisfy a standard relation: subtracting a common vector v from all three arguments yields the same angle as without subtraction.

Русский

Углы после вычитания общего вектора v из всех трёх аргументов удовлетворяют той же зависимости.

LaTeX

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

Lean4

/-- Angles in a vector space are translation invariant -/
@[simp]
theorem angle_sub_const (v₁ v₂ v₃ : V) (v : V) : ∠ (v₁ - v) (v₂ - v) (v₃ - v) = ∠ v₁ v₂ v₃ := by
  simpa only [vsub_eq_sub] using angle_vsub_const v₁ v₂ v₃ v

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