continuousAt_angle — Mathlib

English

For x = (x1, x2) with x1 ≠ 0 and x2 ≠ 0, the map y ↦ angle(y1, y2) is continuous at x.

Русский

Для пары x = (x1, x2) с x1 ≠ 0 и x2 ≠ 0 отображение y ↦ angle(y1, y2) непрерывно в точке x.

LaTeX

$$$$ \text{ContinuousAt}_{x}(\lambda y,\; \angle y_1 y_2) \quad\text{при } x=(x_1,x_2),\; x_1 \neq 0,\; x_2 \neq 0. $$$$

Lean4

theorem continuousAt_angle {x : V × V} (hx1 : x.1 ≠ 0) (hx2 : x.2 ≠ 0) :
    ContinuousAt (fun y : V × V => angle y.1 y.2) x :=
  by
  unfold angle
  fun_prop (disch := simp [*])

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