angle_add_angle_eq_pi_of_angle_eq_pi

English

If ∠BCD = π, then ∠ACB + ∠ACD = π.

Русский

Если ∠BCD = π, тогда ∠ACB + ∠ACD = π.

LaTeX

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

Lean4

/-- If ∠BCD = π, then ∠ACB + ∠ACD = π. -/
nonrec theorem angle_add_angle_eq_pi_of_angle_eq_pi (p₁ : P) {p₂ p₃ p₄ : P} (h : ∠ p₂ p₃ p₄ = π) :
    ∠ p₁ p₃ p₂ + ∠ p₁ p₃ p₄ = π := by
  unfold angle at h
  rw [angle_comm p₁ p₃ p₂, angle_comm p₁ p₃ p₄]
  unfold angle
  exact angle_add_angle_eq_pi_of_angle_eq_pi _ h

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