sin_angle_of_angle_eq_pi_div_two — Mathlib

English

Let ∠ p1 p2 p3 = π/2. Then sin(∠ p2 p3 p1) · dist p3 p2 = dist p1 p3.

Русский

Пусть ∠ p1 p2 p3 = π/2. Тогда sin(∠ p2 p3 p1) · dist(p3,p2) = dist(p1,p3).

LaTeX

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

Lean4

/-- The sine of an angle in a right-angled triangle as a ratio of sides. -/
theorem sin_angle_of_angle_eq_pi_div_two {p₁ p₂ p₃ : P} (h : ∠ p₁ p₂ p₃ = π / 2) (h0 : p₁ ≠ p₂ ∨ p₃ ≠ p₂) :
    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 [← @vsub_ne_zero V, @ne_comm _ p₃, ← @vsub_ne_zero V _ _ _ p₂, or_comm] at h0
  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_of_inner_eq_zero h h0]

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