sin_angle_sub_mul_norm_of_inner_eq_zero

English

Let V be a real inner product space. For any x,y ∈ V with ⟪x,y⟫ = 0, one has sin(angle(x, x − y)) · ||x − y|| = ||y||.

Русский

Пусть V — вещественное пространство с скалярным произведением. Для любых x,y ∈ V с ⟪x,y⟫ = 0 выполняется: sin(∠x(x − y)) · ||x − y|| = ||y||.

LaTeX

$$$ \forall x,y \in V, \ \langle x,y\rangle = 0 \Rightarrow \sin(\angle x (x - y)) \cdot \|x - y\| = \|y\| $$$

Lean4

/-- The sine of an angle in a right-angled triangle multiplied by the hypotenuse equals the
opposite side, version subtracting vectors. -/
theorem sin_angle_sub_mul_norm_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) :
    Real.sin (angle x (x - y)) * ‖x - y‖ = ‖y‖ :=
  by
  rw [← neg_eq_zero, ← inner_neg_right] at h
  rw [sub_eq_add_neg, sin_angle_add_mul_norm_of_inner_eq_zero h, norm_neg]

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