rotation_map — Mathlib

English

Rotation composes compatibly with orientation under linear isomorphisms.

Русский

Поворот совместим с отображением по ориентации через линейное изоморфизмирование.

LaTeX

$$(Orientation.map (Fin 2) f.toLinearEquiv o).rotation θ x = f (o.rotation θ (f.symm x))$$

Lean4

theorem rotation_map (θ : Real.Angle) (f : V ≃ₗᵢ[ℝ] V') (x : V') :
    (Orientation.map (Fin 2) f.toLinearEquiv o).rotation θ x = f (o.rotation θ (f.symm x)) := by
  simp [rotation_apply, o.rightAngleRotation_map]

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