English
Oriented angles vary continuously with nonzero vectors: the map (x,y) ↦ o.oangle(x,y) is continuous at any (x,y) with x ≠ 0 and y ≠ 0.
Русский
Ориентированные углы непрерывны по непрерывным изменениям ненулевых векторов: отображение (x,y) ↦ o.oangle(x,y) непрерывно в точке с x ≠ 0, y ≠ 0.
LaTeX
$$$\text{If } x \neq 0, y \neq 0, \text{ then } (u,v) \mapsto o.oangle(u,v) \text{ is continuous at } (x,y).$$$
Lean4
/-- Oriented angles are continuous when the vectors involved are nonzero. -/
@[fun_prop]
theorem continuousAt_oangle {x : V × V} (hx1 : x.1 ≠ 0) (hx2 : x.2 ≠ 0) :
ContinuousAt (fun y : V × V => o.oangle y.1 y.2) x :=
by
refine (Complex.continuousAt_arg_coe_angle ?_).comp ?_
· exact o.kahler_ne_zero hx1 hx2
exact
((continuous_ofReal.comp continuous_inner).add
((continuous_ofReal.comp o.areaForm'.continuous₂).mul continuous_const)).continuousAt
