angle_right_midpoint_eq_pi_div_two_of_dist_eq

English

If ∠ABC = π, then dist A C = dist A B + dist C B.

Русский

Если ∠ABC = π, то dist(A,C) = dist(A,B) + dist(C,B).

LaTeX

$$$\angle A B C = \pi \Rightarrow dist(A,C) = dist(A,B) + dist(C,B)$$$

Lean4

/-- If M is the midpoint of the segment AB and C is the same distance from A as it is from B
then ∠CMB = π / 2. -/
theorem angle_right_midpoint_eq_pi_div_two_of_dist_eq {p₁ p₂ p₃ : P} (h : dist p₃ p₁ = dist p₃ p₂) :
    ∠ p₃ (midpoint ℝ p₁ p₂) p₂ = π / 2 := by
  rw [midpoint_comm p₁ p₂, angle_left_midpoint_eq_pi_div_two_of_dist_eq h.symm]

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