rightAngleRotationAux₁_rightAngleRotationAux₁

English

For all x, y in E, the inner product ⟪x, o.rightAngleRotationAux₁ y⟫ equals −ω(x, y): ⟪x, o.rightAngleRotationAux₁ y⟫ = −ω(x, y).

Русский

Для любых x, y ∈ E выполнено: ⟪x, o.rightAngleRotationAux₁ y⟫ = −ω(x, y).

LaTeX

$$$\\\\langle x, o.rightAngleRotationAux₁ y\\\\rangle = -\\\\omega(x, y)$$$

Lean4

@[simp]
theorem rightAngleRotationAux₁_rightAngleRotationAux₁ (x : E) :
    o.rightAngleRotationAux₁ (o.rightAngleRotationAux₁ x) = -x :=
  by
  apply ext_inner_left ℝ
  intro y
  have : ⟪o.rightAngleRotationAux₁ y, o.rightAngleRotationAux₁ x⟫ = ⟪y, x⟫ :=
    LinearIsometry.inner_map_map o.rightAngleRotationAux₂ y x
  rw [o.inner_rightAngleRotationAux₁_right, ← o.inner_rightAngleRotationAux₁_left, this, inner_neg_right]

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