rotationAux_apply — Mathlib

English

Let V be a real two-dimensional oriented inner product space and J denote the standard right-angle rotation. For every angle θ and every vector x ∈ V, the auxiliary rotation satisfies o.rotationAux(θ) x = cos(θ) x + sin(θ) Jx.

Русский

Пусть V — ориентированное вещественное двумерное вложенное пространство, а J — стандартное поворот по направлению справа на 90°. Для любого угла θ и любого вектора x ∈ V выполняется: o.rotationAux(θ) x = cos(θ) x + sin(θ) Jx.

LaTeX

$$$ o.rotationAux(\theta) x = \cos\theta\, x + \sin\theta\, J x $$$

Lean4

@[simp]
theorem rotationAux_apply (θ : Real.Angle) (x : V) :
    o.rotationAux θ x = Real.Angle.cos θ • x + Real.Angle.sin θ • J x :=
  rfl

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