English
If φ is a linear isometry equivalence and x ∈ F, then the right-angle rotation commutes with the map: (Orientation.map (Fin 2) φ.toLinearEquiv o).rightAngleRotation x = φ(o.rightAngleRotation (φ^{-1} x)).
Русский
При отображении через изометрическое эквивалентное отображение φ поворот сохраняется: (Orientation.map …).rightAngleRotation x = φ(o.rightAngleRotation (φ^{-1} x)).
LaTeX
$$$\\\\left( Orientation.map (Fin 2) φ^{toLinearEquiv} o \\right).rightAngleRotation\\, x = φ\\left( o.rightAngleRotation (φ^{-1} x) \\right)$$$
Lean4
theorem rightAngleRotation_map {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [hF : Fact (finrank ℝ F = 2)]
(φ : E ≃ₗᵢ[ℝ] F) (x : F) :
(Orientation.map (Fin 2) φ.toLinearEquiv o).rightAngleRotation x = φ (o.rightAngleRotation (φ.symm x)) :=
by
apply ext_inner_right ℝ
intro y
rw [inner_rightAngleRotation_left]
trans ⟪J (φ.symm x), φ.symm y⟫
· simp [o.areaForm_map]
trans ⟪φ (J (φ.symm x)), φ (φ.symm y)⟫
· rw [φ.inner_map_map]
· simp
