angle_add_angle_eq_pi_of_angle_eq_pi

English

If angle x y = π, then the sum of angle x z and angle y z equals π for any vector z.

Русский

Если угол x y равен π, то сумма углов x z и y z по любому z равна π.

LaTeX

$$$\\\\angle x z + \\\\angle y z = \\\\pi$ при $\\\\angle x y = \\\\pi$$$

Lean4

/-- If the angle between two vectors is π, the angles between those
vectors and a third vector add to π. -/
theorem angle_add_angle_eq_pi_of_angle_eq_pi {x y : V} (z : V) (h : angle x y = π) : angle x z + angle y z = π :=
  by
  rcases angle_eq_pi_iff.1 h with ⟨_, ⟨r, ⟨hr, rfl⟩⟩⟩
  rw [angle_smul_left_of_neg x z hr, angle_neg_left, add_sub_cancel]

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