angle_eq_pi_iff — Mathlib

English

The angle between x and y is π if and only if x ≠ 0 and y is a negative multiple of x.

Русский

Угол между x и y равен π тогда и только тогда, когда x ≠ 0 и y есть отрицательный кратный x.

LaTeX

$$$\\\\angle x y = \\\\pi \\\\iff x \\neq 0 \\\\wedge \\\\exists r<0: y = r\\\\cdot x$$$

Lean4

/-- The angle between two vectors is π if and only if they are nonzero
and one is a negative multiple of the other. -/
theorem angle_eq_pi_iff {x y : V} : angle x y = π ↔ x ≠ 0 ∧ ∃ r : ℝ, r < 0 ∧ y = r • x :=
  by
  rw [angle, ← real_inner_div_norm_mul_norm_eq_neg_one_iff, Real.arccos_eq_pi, LE.le.ge_iff_eq']
  exact (abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one x y)).1

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