oangle_sign_sub_left — Mathlib

English

If x and y have equal norms in a 2D real inner product space with orientation o, then the absolute value of the real angle (as a real number) between y − x and y is strictly less than π/2.

Русский

Если нормы x и y равны, то базовый угол между y − x и y по модулю меньше π/2.

LaTeX

$$$\\forall x,y\\in V,\\ \\|x\\| = \\|y\\| \\implies \\Big| (o.oangle(y - x, y)).toReal \\Big| < \\frac{\\pi}{2}$$$

Lean4

/-- Subtracting the second vector passed to `oangle` from the first vector does not change the
sign of the angle. -/
@[simp]
theorem oangle_sign_sub_left (x y : V) : (o.oangle (x - y) y).sign = (o.oangle x y).sign := by
  rw [← o.oangle_sign_sub_smul_left x y 1, one_smul]

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