sameRay_neg_smul_right_iff — Mathlib

English

For any v and r, the vectors −v and r·v are in the same ray exactly when r ≤ 0 or v = 0.

Русский

Для любого v и r векторы −v и r·v лежат в одном луче тогда и только тогда, когда r ≤ 0 или v = 0.

LaTeX

$$$\operatorname{SameRay}(-v,\; r\cdot v) \iff r \le 0 \lor v = 0$$$

Lean4

@[simp]
theorem sameRay_neg_smul_right_iff {v : M} {r : R} : SameRay R (-v) (r • v) ↔ r ≤ 0 ∨ v = 0 := by
  rw [← sameRay_neg_iff, neg_neg, ← neg_smul, sameRay_smul_right_iff, neg_nonneg]

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