oangle_rotation_oangle_right — Mathlib

English

Let V be a 2-dimensional real inner product space with an orientation o. For any vectors x and y in V, the angle between y and the image of x after rotating x by the angle from x to y is zero.

Русский

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

LaTeX

$$$o.oangle\ y\ (o.rotation(o.oangle(x,y))\ x) = 0$$$

Lean4

/-- Rotating the first vector by the angle between the two vectors and swapping the vectors
results in an angle of 0. -/
@[simp]
theorem oangle_rotation_oangle_right (x y : V) : o.oangle y (o.rotation (o.oangle x y) x) = 0 :=
  by
  rw [oangle_rev]
  simp

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