oangle_sign_add_left — Mathlib

English

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

Русский

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

LaTeX

$$$\\forall x,y\\in V,\\ o.oangle(x, x - y).sign = -(o.oangle(x,y).sign)$$$

Lean4

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

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