oangle_left_eq_arccos_of_oangle_eq_pi_div_two

English

Let p1, p2, p3 be points with ∠p1 p2 p3 = π/2. Then ∠p3 p1 p2 = arccos( dist(p1,p2) / dist(p1,p3) ).

Русский

Пусть p1, p2, p3 — точки такие, что ∠p1 p2 p3 = π/2. Тогда ∠p3 p1 p2 = arccos( dist(p1,p2) / dist(p1,p3) ).

LaTeX

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

Lean4

/-- An angle in a right-angled triangle expressed using `arccos`. -/
theorem oangle_left_eq_arccos_of_oangle_eq_pi_div_two {p₁ p₂ p₃ : P} (h : ∡ p₁ p₂ p₃ = ↑(π / 2)) :
    ∡ p₃ p₁ p₂ = Real.arccos (dist 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,
    angle_eq_arccos_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h), dist_comm p₁ p₃]

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