angle₃₂₁_eq_pi — Mathlib

English

If ∠ABC = π then ∠ABC = ∠ABD implies ∠ABD = ∠ACD

Русский

Если ∠ABC = π, то ∠ABC = ∠ABD тогда ∠ABD = ∠ACD.

LaTeX

$$$\angle A B C = \pi \Rightarrow \angle A B D = \angle A C D$$$

Lean4

/-- If the second of three points is strictly between the other two, the angle at that point
(reversed) is π. -/
theorem _root_.Sbtw.angle₃₂₁_eq_pi {p₁ p₂ p₃ : P} (h : Sbtw ℝ p₁ p₂ p₃) : ∠ p₃ p₂ p₁ = π := by
  rw [← h.angle₁₂₃_eq_pi, angle_comm]

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