angle_add_pos_of_inner_eq_zero — Mathlib

English

If x ⟂ y and the triangle is non-degenerate (x = 0 or y ≠ 0), then the angle between x and x + y is positive: 0 < angle(x, x + y).

Русский

Если x перпендикулярно y и треугольник не обделен вырождением (x = 0 или y ≠ 0), то угол между x и x + y положителен: 0 < angle(x, x + y).

LaTeX

$$$$ 0 < \angle x (x+y) $$$$

Lean4

/-- An angle in a non-degenerate right-angled triangle is positive. -/
theorem angle_add_pos_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) (h0 : x = 0 ∨ y ≠ 0) : 0 < angle x (x + y) :=
  by
  rw [angle_add_eq_arccos_of_inner_eq_zero h, Real.arccos_pos, norm_add_eq_sqrt_iff_real_inner_eq_zero.2 h]
  by_cases hx : x = 0; · simp [hx]
  rw [div_lt_one
      (Real.sqrt_pos.2 (Left.add_pos_of_pos_of_nonneg (mul_self_pos.2 (norm_ne_zero_iff.2 hx)) (mul_self_nonneg _))),
    Real.lt_sqrt (norm_nonneg _), pow_two]
  simpa [hx] using h0

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