oangle_sign_sub_smul_left — Mathlib

English

Let V be a 2D real inner product space with orientation o. For any x,y and real r, the sign of o.oangle(x, y - r·x) equals the sign of o.oangle(x,y).

Русский

Пусть V — двумерное пространство над ℝ с ориентировкой o. Для любых x,y и r знак угла между x и y - r·x равен знаку угла между x и y.

LaTeX

$$$\\forall x,y\\in V,\\ r\\in\\mathbb{R},\\ \\operatorname{sign}\\big(o.oangle(x, y - r\\,x)\\big) = \\operatorname{sign}\\big(o.oangle(x,y)\\big)$$$

Lean4

/-- Subtracting a multiple of the second vector passed to `oangle` from the first vector does
not change the sign of the angle. -/
@[simp]
theorem oangle_sign_sub_smul_left (x y : V) (r : ℝ) : (o.oangle (x - r • y) y).sign = (o.oangle x y).sign := by
  rw [sub_eq_add_neg, ← neg_smul, oangle_sign_add_smul_left]

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