tan_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two

English

The norm of y divided by the cosine of the angle o.oangle(y, y−x) equals the length of y−x.

Русский

Норма ||y|| деленная на косинус угла o.oangle(y, y−x) равна длине ||y−x||.

LaTeX

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

Lean4

/-- The tangent of an angle in a right-angled triangle multiplied by the adjacent side equals
the opposite side, version subtracting vectors. -/
theorem tan_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = ↑(π / 2)) :
    Real.Angle.tan (o.oangle y (y - x)) * ‖y‖ = ‖x‖ :=
  by
  have hs : (o.oangle y (y - x)).sign = 1 := by rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]
  rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.tan_coe,
    InnerProductGeometry.tan_angle_sub_mul_norm_of_inner_eq_zero (o.inner_rev_eq_zero_of_oangle_eq_pi_div_two h)
      (Or.inl (o.right_ne_zero_of_oangle_eq_pi_div_two h))]

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