dist_eq_dist_mul_sin_angle_div_sin_angle

English

If points are not collinear, then dist(p1,p2) = dist(p3,p1) * sin(angle p2 p3 p1) / sin(angle p1 p2 p3).

Русский

Если точки не лежат на одной прямой, то dist(p1,p2) = dist(p3,p1) * sin(angle p2 p3 p1) / sin(angle p1 p2 p3).

LaTeX

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

Lean4

/-- A variant of the law of sines, requiring that the points not be collinear. -/
theorem dist_eq_dist_mul_sin_angle_div_sin_angle {p₁ p₂ p₃ : P} (h : ¬Collinear ℝ ({ p₁, p₂, p₃ } : Set P)) :
    dist p₁ p₂ = dist p₃ p₁ * Real.sin (∠ p₂ p₃ p₁) / Real.sin (∠ p₁ p₂ p₃) :=
  by
  have sin_gt_zero : 0 < Real.sin (∠ p₁ p₂ p₃) := sin_pos_of_not_collinear h
  field_simp
  rw [mul_comm, mul_comm (dist p₃ p₁), law_sin]

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