norm_div_cos_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 ||x|| / cos(angle(x, x − y)) = ||x − y||.

Русский

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

LaTeX

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

Lean4

/-- A side of a right-angled triangle divided by the cosine of the adjacent angle equals the
hypotenuse, version subtracting vectors. -/
theorem norm_div_cos_angle_sub_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) (h0 : x ≠ 0 ∨ y = 0) :
    ‖x‖ / Real.cos (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, norm_div_cos_angle_add_of_inner_eq_zero h h0]

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