tan_angle_add_mul_norm_of_inner_eq_zero

English

For ⟪x, y⟫ = 0 and x ≠ 0 or y ≠ 0, the following holds: ||x|| / cos(angle(x, x + y)) = ||x + y||.

Русский

Для ⟪x, y⟫ = 0 и (x ≠ 0 или y ≠ 0) выполняется: ||x|| / cos(angle(x, x + y)) = ||x + y||.

LaTeX

$$$$ \frac{\|x\|}{\cos\big( \angle x (x+y) \big)} = \|x+y\| $$$$

Lean4

/-- The tangent of an angle in a right-angled triangle multiplied by the adjacent side equals
the opposite side. -/
theorem tan_angle_add_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 [tan_angle_add_of_inner_eq_zero h]
  rcases h0 with (h0 | h0) <;> simp [h0]

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