English
Let v, v1, v2, v3 be vectors in a real inner product space. Translating all three points by the same vector v does not change the angle formed by the three points; equivalently, the angle formed by (v − v1), (v − v2), (v − v3) equals the angle formed by v1, v2, v3.
Русский
Пусть v, v1, v2, v3 — векторы в вещественном пространстве с обычным скалярным произведением. При переносе всех трёх точек на один и тот же вектор v угол, образованный этими точками, не меняется; эквивалентно равенству угла ∠(v−v1)(v−v2)(v−v3) = ∠v1v2v3.
LaTeX
$$$\angle(v - v_1)
(v - v_2)
(v - v_3) = \angle v_1 v_2 v_3$$$
Lean4
/-- Angles in a vector space are invariant to inversion -/
@[simp]
theorem angle_const_sub (v : V) (v₁ v₂ v₃ : V) : ∠ (v - v₁) (v - v₂) (v - v₃) = ∠ v₁ v₂ v₃ := by
simpa only [vsub_eq_sub] using angle_const_vsub v v₁ v₂ v₃
