tan_angle_sub_mul_norm_of_inner_eq_zero

English

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

Русский

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

LaTeX

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

Lean4

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

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