angle_sub_eq_angle_sub_rev_of_norm_eq

English

If two vectors x and y have equal norms, then the angle formed by x and x−y equals the angle formed by y and y−x.

Русский

Если нормы векторов x и y равны, то угол между x и x−y равен углу между y и y−x.

LaTeX

$$$\|x\| = \|y\| \Rightarrow \angle x (x-y) = \angle y (y-x)$$$

Lean4

/-- **Pons asinorum**, vector angle form. -/
theorem angle_sub_eq_angle_sub_rev_of_norm_eq {x y : V} (h : ‖x‖ = ‖y‖) : angle x (x - y) = angle y (y - x) :=
  by
  refine Real.injOn_cos ⟨angle_nonneg _ _, angle_le_pi _ _⟩ ⟨angle_nonneg _ _, angle_le_pi _ _⟩ ?_
  rw [cos_angle, cos_angle, h, ← neg_sub, norm_neg, neg_sub, inner_sub_right, inner_sub_right,
    real_inner_self_eq_norm_mul_norm, real_inner_self_eq_norm_mul_norm, h, real_inner_comm x y]

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