dist_div_sin_angle_of_angle_eq_pi_div_two

English

An angle in a nondegenerate right-angled triangle is positive.

Русский

Угол в не вырожденном прямоугольном треугольнике положителен.

LaTeX

$$$ 0 < \angle p_2 p_3 p_1 $$$

Lean4

/-- A side of a right-angled triangle divided by the sine of the opposite angle equals the
hypotenuse. -/
theorem dist_div_sin_angle_of_angle_eq_pi_div_two {p₁ p₂ p₃ : P} (h : ∠ p₁ p₂ p₃ = π / 2) (h0 : p₁ ≠ p₂ ∨ p₃ = p₂) :
    dist p₁ p₂ / Real.sin (∠ p₂ 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 [eq_comm, ← @vsub_ne_zero V, ← @vsub_eq_zero_iff_eq V, 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,
    norm_div_sin_angle_add_of_inner_eq_zero h h0]

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