angle_eq_angle_of_angle_eq_pi_of_angle_eq_pi

English

If ∠BCD = π, then for any point A, ∠ABC = ∠ABD.

Русский

Если ∠BCD = π, то для произвольной точки A углы ∠ABC и ∠ABD равны.

LaTeX

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

Lean4

/-- **Vertical Angles Theorem**: angles opposite each other, formed by two intersecting straight
lines, are equal. -/
theorem angle_eq_angle_of_angle_eq_pi_of_angle_eq_pi {p₁ p₂ p₃ p₄ p₅ : P} (hapc : ∠ p₁ p₅ p₃ = π)
    (hbpd : ∠ p₂ p₅ p₄ = π) : ∠ p₁ p₅ p₂ = ∠ p₃ p₅ p₄ := by
  linarith [angle_add_angle_eq_pi_of_angle_eq_pi p₁ hbpd, angle_comm p₄ p₅ p₁,
    angle_add_angle_eq_pi_of_angle_eq_pi p₄ hapc, angle_comm p₄ p₅ p₃]

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