oangle₂₁₃_eq_zero — Mathlib

English

If B is weakly between A and C (Wbtw), then the oriented angle at A in the triple (A,B,C) is zero: ∡ B A C = 0.

Русский

Если B лежит между A и C (слабая между), то ориентированный угол в точке A равен нулю: ∡ B A C = 0.

LaTeX

$$$Wbtw\ Real\ p_1 p_2 p_3 \Rightarrow \angle p_2 p_1 p_3 = 0$$$

Lean4

/-- If the second of three points is weakly between the other two, the oriented angle at the
first point is zero. -/
theorem _root_.Wbtw.oangle₂₁₃_eq_zero {p₁ p₂ p₃ : P} (h : Wbtw ℝ p₁ p₂ p₃) : ∡ p₂ p₁ p₃ = 0 :=
  by
  by_cases hp₂p₁ : p₂ = p₁; · simp [hp₂p₁]
  by_cases hp₃p₁ : p₃ = p₁; · simp [hp₃p₁]
  rw [oangle_eq_zero_iff_angle_eq_zero hp₂p₁ hp₃p₁]
  exact h.angle₂₁₃_eq_zero_of_ne hp₂p₁

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