dist_eq_abs_sub_dist_of_angle_eq_zero

English

If ∠ABC = 0, then dist A C = |dist A B − dist C B|.

Русский

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

LaTeX

$$$\angle A B C = 0 \Rightarrow dist(A,C) = |dist(A,B) - dist(C,B)|$$$

Lean4

/-- If ∠ABC = 0, then (dist A C) = abs ((dist A B) - (dist B C)). -/
theorem dist_eq_abs_sub_dist_of_angle_eq_zero {p₁ p₂ p₃ : P} (h : ∠ p₁ p₂ p₃ = 0) :
    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_abs_sub_norm_of_angle_eq_zero h

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