eq_iff_norm_eq_and_oangle_eq_zero

English

x = y iff their norms are equal and the oriented angle between them is zero.

Русский

x = y тогда и только тогда, когда их нормы равны и между ними нулевой ориентированный угол.

LaTeX

$$$x = y \iff \|x\| = \|y\| \land o.oangle x y = 0$$$

Lean4

/-- Two vectors are equal if and only if they have equal norms and zero angle between them. -/
theorem eq_iff_norm_eq_and_oangle_eq_zero (x y : V) : x = y ↔ ‖x‖ = ‖y‖ ∧ o.oangle x y = 0 :=
  by
  rw [oangle_eq_zero_iff_sameRay]
  constructor
  · rintro rfl
    simp; rfl
  · rcases eq_or_ne y 0 with (rfl | hy)
    · simp
    rintro ⟨h₁, h₂⟩
    obtain ⟨r, hr, rfl⟩ := h₂.exists_nonneg_right hy
    have : ‖y‖ ≠ 0 := by simpa using hy
    obtain rfl : r = 1 := by
      apply mul_right_cancel₀ this
      simpa [norm_smul, abs_of_nonneg hr] using h₁
    simp

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