angle₂₁₃_eq_zero_of_ne — Mathlib

English

If the midpoint M of AB and C is equidistant from A and B, then ∠CMA = π/2.

Русский

Если M — середина AB и CA = CB, тогда ∠CMA = π/2.

LaTeX

$$$dist(C,A) = dist(C,B) \Rightarrow \angle C M A = \frac{\pi}{2}$$$

Lean4

/-- If the second of three points is weakly between the other two, and not equal to the first,
the angle at the first point is zero. -/
theorem _root_.Wbtw.angle₂₁₃_eq_zero_of_ne {p₁ p₂ p₃ : P} (h : Wbtw ℝ p₁ p₂ p₃) (hp₂p₁ : p₂ ≠ p₁) : ∠ p₂ p₁ p₃ = 0 :=
  by
  rw [angle, angle_eq_zero_iff]
  rcases h with ⟨r, ⟨hr0, hr1⟩, rfl⟩
  have hr0' : r ≠ 0 := by
    rintro rfl
    simp at hp₂p₁
  replace hr0 := hr0.lt_of_ne hr0'.symm
  refine ⟨vsub_ne_zero.2 hp₂p₁, r⁻¹, inv_pos.2 hr0, ?_⟩
  rw [AffineMap.lineMap_apply, vadd_vsub_assoc, vsub_self, add_zero, smul_smul, inv_mul_cancel₀ hr0', one_smul]

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