equiv_neg_iff — Mathlib

English

For RayVector, negation preserves equivalence: -v1 ≈ -v2 iff v1 ≈ v2.

Русский

Для RayVector отрицание сохраняет эквивалентность: -v1 ≈ -v2 эквивалентно v1 ≈ v2.

LaTeX

$$$-v_1 \approx -v_2 \iff v_1 \approx v_2$ for RayVector R M.$$

Lean4

/-- If two nonzero vectors are equivalent, so are their negations. -/
@[simp]
theorem equiv_neg_iff {v₁ v₂ : RayVector R M} : -v₁ ≈ -v₂ ↔ v₁ ≈ v₂ :=
  sameRay_neg_iff

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