neg_rayOfNeZero — Mathlib

English

Negating the zero-free vector ray flips the sign inside the ray correctly: -rayOfNeZero(v) = rayOfNeZero(-v).

Русский

Отрицание луча без нуля соответствует изменению знака в векторе: -rayOfNeZero(v) = rayOfNeZero(-v).

LaTeX

$$$-\text{rayOfNeZero}(R, v, h) = \text{rayOfNeZero}(R, -v, \text{neg}(h))$$$

Lean4

/-- The ray given by the negation of a nonzero vector. -/
@[simp]
theorem neg_rayOfNeZero (v : M) (h : v ≠ 0) : -rayOfNeZero R _ h = rayOfNeZero R (-v) (neg_ne_zero.2 h) :=
  rfl

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