sameRay_smul_right_iff_of_ne — Mathlib

English

If v ≠ 0 and r ≠ 0, then SameRay(R, v, r·v) iff 0 < r.

Русский

Если v ≠ 0 и r ≠ 0, тогда SameRay(v, r·v) эквивално 0 < r.

LaTeX

$$$SameRay(R,v, r\cdot v) \iff 0

Lean4

/-- A nonzero vector is in the same ray as a multiple of itself if and only if that multiple
is positive. -/
theorem sameRay_smul_right_iff_of_ne {v : M} (hv : v ≠ 0) {r : R} (hr : r ≠ 0) : SameRay R v (r • v) ↔ 0 < r := by
  simp only [sameRay_smul_right_iff, hv, or_false, hr.symm.le_iff_lt]

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