dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two

English

In a right-angled configuration, dist(p1,p3)^2 = dist(p1,p2)^2 + dist(p3,p2)^2 if and only if ∠ p1 p2 p3 = π/2.

Русский

В прямоугольной конфигурации выполняется равенство расстояний по Пифагору ⇔ угол ∠ p1 p2 p3 равен π/2.

LaTeX

$$$ dist(p_1,p_3)^2 = dist(p_1,p_2)^2 + dist(p_3,p_2)^2 \quad \Longleftrightarrow \quad \angle p_1 p_2 p_3 = \frac{\pi}{2} $$$

Lean4

/-- **Pythagorean theorem**, if-and-only-if angle-at-point form. -/
theorem dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two (p₁ p₂ p₃ : P) :
    dist p₁ p₃ * dist p₁ p₃ = dist p₁ p₂ * dist p₁ p₂ + dist p₃ p₂ * dist p₃ p₂ ↔ ∠ p₁ p₂ p₃ = π / 2 := by
  erw [dist_comm p₃ p₂, dist_eq_norm_vsub V p₁ p₃, dist_eq_norm_vsub V p₁ p₂, dist_eq_norm_vsub V p₂ p₃, ←
    norm_sub_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two, vsub_sub_vsub_cancel_right p₁, ←
    neg_vsub_eq_vsub_rev p₂ p₃, norm_neg]

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