oangle_sub_left_eq_arctan_of_oangle_eq_pi_div_two

English

Let V be a two-dimensional real normed space with an inner product and o an orientation. If the oriented angle between x and y is π/2, then the oriented angle between x−y and x equals arctan(||y||/||x||).

Русский

Пусть V — двумерное вещественное пространство с скобами нормы и внутренним произведением, а o — ориентация. Если ориентированный угол o.oangle(x, y) = π/2, то угол o.oangle(x−y, x) равен arctan(||y||/||x||).

LaTeX

$$$ o.oangle(x - y, x) = \arctan\left(\frac{\|y\|}{\|x\|}\right) $$$

Lean4

/-- An angle in a right-angled triangle expressed using `arctan`, version subtracting vectors. -/
theorem oangle_sub_left_eq_arctan_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = ↑(π / 2)) :
    o.oangle (x - y) x = Real.arctan (‖y‖ / ‖x‖) :=
  by
  rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
  exact (-o).oangle_sub_right_eq_arctan_of_oangle_eq_pi_div_two h

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