rightAngleRotation_map' — Mathlib

English

There is a map for rightAngleRotation under a morphism φ: (Orientation.map (Fin 2) φ.toLinearEquiv o).rightAngleRotation = (φ.symm.trans o.rightAngleRotation).trans φ.

Русский

Сохранение поворота через отображение: (Orientation.map (Fin 2) φ.toLinearEquiv o).rightAngleRotation = (φ.symm.trans o.rightAngleRotation).trans φ.

LaTeX

$$$( Orientation.map (Fin 2) φ.toLinearEquiv o).rightAngleRotation = (φ^{-1}.trans o.rightAngleRotation).trans φ$$$

Lean4

theorem rightAngleRotation_map' {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [Fact (finrank ℝ F = 2)]
    (φ : E ≃ₗᵢ[ℝ] F) :
    (Orientation.map (Fin 2) φ.toLinearEquiv o).rightAngleRotation = (φ.symm.trans o.rightAngleRotation).trans φ :=
  LinearIsometryEquiv.ext <| o.rightAngleRotation_map φ

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