dist_eq_add_dist_iff_angle_eq_pi — Mathlib

English

If A ≠ B and C ≠ B, then ∠ABC = π if and only if dist A C = |dist A B − dist C B|.

Русский

Если A ≠ B и C ≠ B, тогда ∠ABC = π тогда и только тогда, когда dist(A,C) = |dist(A,B) − dist(C,B)|.

LaTeX

$$$\angle A B C = \pi \iff dist(A,C) = |dist(A,B) - dist(C,B)| \, (A\neq B,\; C\neq B)$$$

Lean4

/-- If A ≠ B and C ≠ B then ∠ABC = π if and only if (dist A C) = (dist A B) + (dist B C). -/
theorem dist_eq_add_dist_iff_angle_eq_pi {p₁ p₂ p₃ : P} (hp₁p₂ : p₁ ≠ p₂) (hp₃p₂ : p₃ ≠ p₂) :
    dist p₁ p₃ = dist p₁ p₂ + dist p₃ p₂ ↔ ∠ p₁ 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_iff_angle_eq_pi (fun he => hp₁p₂ (vsub_eq_zero_iff_eq.1 he)) fun he =>
      hp₃p₂ (vsub_eq_zero_iff_eq.1 he)

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