sin_angle_mul_dist_of_angle_eq_pi_div_two

English

In the same right-angle setting, dist(p1,p3) = dist(p1,p2) / sin(∠ p2 p3 p1).

Русский

В той же прямоугольной конфигурации dist(p1,p3) = dist(p1,p2) / sin(∠ p2 p3 p1).

LaTeX

$$$ \operatorname{dist}(p_1,p_3) = \dfrac{\operatorname{dist}(p_1,p_2)}{\sin(\angle p_2 p_3 p_1)} $$$

Lean4

/-- The sine of an angle in a right-angled triangle multiplied by the hypotenuse equals the
opposite side. -/
theorem sin_angle_mul_dist_of_angle_eq_pi_div_two {p₁ p₂ p₃ : P} (h : ∠ p₁ p₂ p₃ = π / 2) :
    Real.sin (∠ p₂ p₃ p₁) * dist p₁ p₃ = dist p₁ p₂ :=
  by
  rw [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, real_inner_comm, ← neg_eq_zero, ← inner_neg_left,
    neg_vsub_eq_vsub_rev] at h
  rw [angle, dist_eq_norm_vsub V p₁ p₂, dist_eq_norm_vsub V p₁ p₃, ← vsub_add_vsub_cancel p₁ p₂ p₃, add_comm,
    sin_angle_add_mul_norm_of_inner_eq_zero h]

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