tan_oangle_add_left_of_oangle_eq_pi_div_two

English

If o.oangle x y = π/2, then tan of the angle between (x+y) and y equals ||x|| / ||y||.

Русский

Если o.oangle x y = π/2, то тангенс угла между (x+y) и y равен ||x|| / ||y||.

LaTeX

$$$ o.oangle x y = \uparrow\left( \frac{\pi}{2} \right) \Rightarrow \tan\left(o.oangle (x+y) y\right) = \frac{\|x\|}{\|y\|} $$$

Lean4

/-- The tangent of an angle in a right-angled triangle as a ratio of sides. -/
theorem tan_oangle_add_left_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = ↑(π / 2)) :
    Real.Angle.tan (o.oangle (x + y) y) = ‖x‖ / ‖y‖ :=
  by
  rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
  rw [add_comm]
  exact (-o).tan_oangle_add_right_of_oangle_eq_pi_div_two h

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