angle_add_lt_pi_div_two_of_inner_eq_zero

English

For ⟪x, y⟫ = 0 and x ≠ 0, the angle between x and x + y is less than π/2: angle(x, x + y) < π/2.

Русский

При ⟪x, y⟫ = 0 и x ≠ 0 угол между x и x + y меньше π/2: angle(x, x + y) < π/2.

LaTeX

$$$$ \angle x (x+y) < \frac{\pi}{2} $$$$

Lean4

/-- An angle in a non-degenerate right-angled triangle is less than `π / 2`. -/
theorem angle_add_lt_pi_div_two_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) (h0 : x ≠ 0) : angle x (x + y) < π / 2 :=
  by
  rw [angle_add_eq_arccos_of_inner_eq_zero h, Real.arccos_lt_pi_div_two, norm_add_eq_sqrt_iff_real_inner_eq_zero.2 h]
  exact
    div_pos (norm_pos_iff.2 h0)
      (Real.sqrt_pos.2 (Left.add_pos_of_pos_of_nonneg (mul_self_pos.2 (norm_ne_zero_iff.2 h0)) (mul_self_nonneg _)))

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