angle_add_le_pi_div_two_of_inner_eq_zero

English

If x ⟪x, y⟫ = 0 and x ≠ 0, then angle(x, x + y) = arctan( ||y|| / ||x|| ).

Русский

Если ⟪x, y⟫ = 0 и x ≠ 0, то угол между x и x + y равен arctan( ||y|| / ||x|| ).

LaTeX

$$$$ \angle x (x+y) = \arctan\left( \frac{\|y\|}{\|x\|} \right) $$$$

Lean4

/-- An angle in a right-angled triangle is at most `π / 2`. -/
theorem angle_add_le_pi_div_two_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) : angle x (x + y) ≤ π / 2 :=
  by
  rw [angle_add_eq_arccos_of_inner_eq_zero h, Real.arccos_le_pi_div_two]
  exact div_nonneg (norm_nonneg _) (norm_nonneg _)

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