tan_oangle_right_of_oangle_eq_pi_div_two

English

If ∡ p1 p2 p3 = π/2, then tan(∡ p2 p3 p1) = dist(p1,p2) / dist(p3,p2).

Русский

Если ∡ p1 p2 p3 = π/2, то tan(∡ p2 p3 p1) = dist(p1,p2) / dist(p3,p2).

LaTeX

$$$\tan\left(\angle p_2 p_3 p_1\right) = \frac{\operatorname{dist}(p_1,p_2)}{\operatorname{dist}(p_3,p_2)} \quad\text{при } \angle p_1 p_2 p_3 = \frac{\pi}{2}$$$

Lean4

/-- The tangent of an angle in a right-angled triangle as a ratio of sides. -/
theorem tan_oangle_right_of_oangle_eq_pi_div_two {p₁ p₂ p₃ : P} (h : ∡ p₁ p₂ p₃ = ↑(π / 2)) :
    Real.Angle.tan (∡ p₂ p₃ p₁) = dist p₁ p₂ / dist p₃ p₂ :=
  by
  have hs : (∡ p₂ p₃ p₁).sign = 1 := by rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
  rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.tan_coe,
    tan_angle_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)]

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