eq_iff_oangle_eq_zero_of_norm_eq — Mathlib

English

If the oriented angle is zero, equality is equivalent to equality of norms.

Русский

Если угол равен нулю, равенство x = y эквивалентно равенству норм.

LaTeX

$$$o.oangle x y = 0 \Rightarrow (x = y \iff \|x\| = \|y\|)$$$

Lean4

/-- Two vectors with equal norms are equal if and only if they have zero angle between them. -/
theorem eq_iff_oangle_eq_zero_of_norm_eq {x y : V} (h : ‖x‖ = ‖y‖) : x = y ↔ o.oangle x y = 0 :=
  ⟨fun he => ((o.eq_iff_norm_eq_and_oangle_eq_zero x y).1 he).2, fun ha =>
    (o.eq_iff_norm_eq_and_oangle_eq_zero x y).2 ⟨h, ha⟩⟩

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