angle_left_midpoint_eq_pi_div_two_of_dist_eq

English

The angle between three points is π if and only if the second point lies strictly between the first and the third.

Русский

Угол между тремя точками равен π тогда, когда вторая точка лежит строго между первой и третьей.

LaTeX

$$$\angle p_1 p_2 p_3 = \pi \iff Sbtw\; p_1\; p_2\; p_3$$$

Lean4

/-- If M is the midpoint of the segment AB and C is the same distance from A as it is from B
then ∠CMA = π / 2. -/
theorem angle_left_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
  let m : P := midpoint ℝ p₁ p₂
  have h1 : p₃ -ᵥ p₁ = p₃ -ᵥ m - (p₁ -ᵥ m) := (vsub_sub_vsub_cancel_right p₃ p₁ m).symm
  have h2 : p₃ -ᵥ p₂ = p₃ -ᵥ m + (p₁ -ᵥ m) := by rw [left_vsub_midpoint, ← midpoint_vsub_right, vsub_add_vsub_cancel]
  rw [dist_eq_norm_vsub V p₃ p₁, dist_eq_norm_vsub V p₃ p₂, h1, h2] at h
  exact (norm_add_eq_norm_sub_iff_angle_eq_pi_div_two (p₃ -ᵥ m) (p₁ -ᵥ m)).mp h.symm

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