angle_sub_pos_of_inner_eq_zero — Mathlib

English

If ⟪x, y⟫ = 0 and x ≠ 0 ∨ y ≠ 0, then 0 < angle(x, x − y).

Русский

Если ⟪x, y⟫ = 0 и x ≠ 0 или y ≠ 0, то 0 < angle(x, x − y).

LaTeX

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

Lean4

/-- An angle in a non-degenerate right-angled triangle is positive, version subtracting
vectors. -/
theorem angle_sub_pos_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) (h0 : x = 0 ∨ y ≠ 0) : 0 < angle x (x - y) :=
  by
  rw [← neg_eq_zero, ← inner_neg_right] at h
  rw [← neg_ne_zero] at h0
  rw [sub_eq_add_neg]
  exact angle_add_pos_of_inner_eq_zero h h0

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