English
Suppose o is an orientation on a 2D real space V and f is a real-linear isomorphism V ≃ᵢ[ℝ] ℂ with Orientation.map (Fin 2) f.toLinearEquiv o = Complex.orientation. Then for all x,y ∈ V, o.oangle x y = Complex.arg (conj (f x) ⋅ f y).
Русский
Пусть есть ориентирование o на 2D-пространстве V и f — ре-линейное изоморфизм V ≃ᵢ[ℝ] ℂ так, что Orientation.map (Fin 2) f.toLinearEquiv o = Complex.orientation. Тогда для любых x,y ∈ V выполняется o.oangle x y = Complex.arg (conj (f x) ⋅ f y).
LaTeX
$$$ Orientation.map (Fin 2) f.toLinearEquiv o = Complex.orientation \Rightarrow \forall x,y\in V,\ o.oangle x y = Complex.arg (\overline{f x} \cdot f y) $$$
Lean4
/-- The oriented angle on an oriented real inner product space of dimension 2 can be evaluated in
terms of a complex-number representation of the space. -/
theorem oangle_map_complex (f : V ≃ₗᵢ[ℝ] ℂ) (hf : Orientation.map (Fin 2) f.toLinearEquiv o = Complex.orientation)
(x y : V) : o.oangle x y = Complex.arg (conj (f x) * f y) :=
by
rw [← Complex.oangle, ← hf, o.oangle_map]
iterate 2 rw [LinearIsometryEquiv.symm_apply_apply]
