oangle_sign_sub_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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