English
Let o be an orientation of a 2D real space V, x,y ∈ V', and f a real-linear isometry V ≃ᵢ[ℝ] V'. Then the angle with respect to the mapped orientation equals the angle with respect to the original orientation on the inverse images: (Orientation.map (Fin 2) f.toLinearEquiv o).oangle x y = o.oangle (f.symm x) (f.symm y).
Русский
Пусть o — ориентирование пространства V размерности 2, x,y ∈ V', и f — линейное изометрическое отображение V в V'. Тогда угол с учётом отображённого ориентирования равен углу с учётом исходного ориентирования между образами обратно через f-обратное.
LaTeX
$$$ (Orientation.map (Fin 2) f.toLinearEquiv o).oangle x y = o.oangle (f.symm x) (f.symm y) $$$
Lean4
/-- The angle between two vectors, with respect to an orientation given by `Orientation.map`
with a linear isometric equivalence, equals the angle between those two vectors, transformed by
the inverse of that equivalence, with respect to the original orientation. -/
@[simp]
theorem oangle_map (x y : V') (f : V ≃ₗᵢ[ℝ] V') :
(Orientation.map (Fin 2) f.toLinearEquiv o).oangle x y = o.oangle (f.symm x) (f.symm y) := by
simp [oangle, o.kahler_map]
