angle₃₁₂_eq_zero_of_ne — Mathlib

English

If the second of three points is weakly between the other two, and not equal to the first, the angle at the first point (reversed) is zero.

Русский

Если вторая из трёх точек лежит между двумя другими и не равна первой, угол в первой точке (обратно) ноль.

LaTeX

$$$Wbtw\; p_1\; p_2\; p_3 \land p_2 \neq p_1 \Rightarrow \angle p_3 p_1 p_2 = 0$$$

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 (reversed) 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 [← h.angle₂₁₃_eq_zero_of_ne hp₂p₁, angle_comm]

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