angle_eq_zero_iff — Mathlib

English

The angle between x and y is zero if and only if x ≠ 0 and y is a positive multiple of x.

Русский

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

LaTeX

$$$\\\\angle x y = 0 \\\\Longleftrightarrow x \\neq 0 \\wedge \\\\exists r>0: y = r\\\\cdot x$$$

Lean4

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

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