angle_eq_arctan_of_angle_eq_pi_div_two

English

If ∠ p1 p2 p3 = π/2, then ∠ p2 p3 p1 = arctan(dist(p1,p2) / dist(p3,p2)).

Русский

Если ∠ p1 p2 p3 = π/2, то ∠ p2 p3 p1 = arctan(dist(p1,p2) / dist(p3,p2)).

LaTeX

$$$ \angle p_2 p_3 p_1 = \arctan\left( \dfrac{\operatorname{dist}(p_1,p_2)}{\operatorname{dist}(p_3,p_2)} \right) $$$

Lean4

/-- An angle in a right-angled triangle expressed using `arctan`. -/
theorem angle_eq_arctan_of_angle_eq_pi_div_two {p₁ p₂ p₃ : P} (h : ∠ p₁ p₂ p₃ = π / 2) (h0 : p₃ ≠ p₂) :
    ∠ p₂ p₃ p₁ = Real.arctan (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 [ne_comm, ← @vsub_ne_zero V] 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,
    angle_add_eq_arctan_of_inner_eq_zero h h0]

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