dist_div_cos_oangle_left_of_oangle_eq_pi_div_two

English

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

Русский

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

LaTeX

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

Lean4

/-- A side of a right-angled triangle divided by the cosine of the adjacent angle equals the
hypotenuse. -/
theorem dist_div_cos_oangle_left_of_oangle_eq_pi_div_two {p₁ p₂ p₃ : P} (h : ∡ p₁ p₂ p₃ = ↑(π / 2)) :
    dist p₁ p₂ / Real.Angle.cos (∡ p₃ 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, angle_comm, Real.Angle.cos_coe, dist_comm p₁ p₃,
    dist_div_cos_angle_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inr (left_ne_of_oangle_eq_pi_div_two h))]

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