dist_eq_add_dist_of_angle_eq_pi — Mathlib

English

If A ≠ B and C ≠ B, dist A C = dist A B + dist C B if and only if ∠ABC = π.

Русский

Если A ≠ B и C ≠ B, расстояние AC равно AB+CB тогда и только тогда, когда ∠ABC = π.

LaTeX

$$$\angle A B C = \pi \iff dist(A,C) = dist(A,B) + dist(C,B)$ при $A\neq B$, $C\neq B$$$

Lean4

/-- If ∠ABC = π, then (dist A C) = (dist A B) + (dist B C). -/
theorem dist_eq_add_dist_of_angle_eq_pi {p₁ p₂ p₃ : P} (h : ∠ p₁ p₂ p₃ = π) : dist p₁ p₃ = dist p₁ p₂ + dist p₃ p₂ :=
  by
  rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, dist_eq_norm_vsub V, ← vsub_sub_vsub_cancel_right]
  exact norm_sub_eq_add_norm_of_angle_eq_pi h

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