norm_div_tan_angle_sub_of_inner_eq_zero

English

Let V be a real inner product space. If ⟪x,y⟫ = 0 and (x = 0 ∨ y ≠ 0), then ||y|| / tan(angle(x, x − y)) = ||x||.

Русский

Пусть V — вещественное пространство с скалярным произведением. При условии ⟪x,y⟫ = 0 и (x = 0 или y ≠ 0) выполняется ||y|| / tan(∠x(x − y)) = ||x||.

LaTeX

$$$ \forall x,y \in V,\ \langle x,y\rangle = 0 \Rightarrow (x = 0 \lor y \neq 0) \Rightarrow \frac{\|y\|}{\tan(\angle x (x - y))} = \|x\| $$$

Lean4

/-- A side of a right-angled triangle divided by the tangent of the opposite angle equals the
adjacent side, version subtracting vectors. -/
theorem norm_div_tan_angle_sub_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) (h0 : x = 0 ∨ y ≠ 0) :
    ‖y‖ / Real.tan (angle x (x - y)) = ‖x‖ :=
  by
  rw [← neg_eq_zero, ← inner_neg_right] at h
  rw [← neg_ne_zero] at h0
  rw [sub_eq_add_neg, ← norm_neg, norm_div_tan_angle_add_of_inner_eq_zero h h0]

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