sameRay_neg_swap

Mathlib.LinearAlgebra.Ray

URI: https://scilib.ai/kg/mathlib#sameRay_neg_swap

English

Negating a ray swaps the sign of the vector in the ray relation: SameRay(-x,y) iff SameRay(x,-y).

Русский

Отрицание луча меняет знак в связке лучей: SameRay(-x,y) эквивалентно SameRay(x,-y).

LaTeX

$$$\text{SameRay}( -x, y) \iff \text{SameRay}( x, -y).$$$

Lean4

theorem sameRay_neg_swap : SameRay R (-x) y ↔ SameRay R x (-y) := by rw [← sameRay_neg_iff, neg_neg]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru