ray_pos_smul — Mathlib

English

The ray of a positive multiple of a nonzero vector equals the ray of the vector itself.

Русский

Луч положительного множителя ненулевого вектора совпадает с лучом самого вектора.

LaTeX

$$@[simp] $ \operatorname{rayOfNeZero}(R, r \cdot v) = \operatorname{rayOfNeZero}(R, v) $ for 0 < r and v ≠ 0.$$

Lean4

/-- The ray given by a positive multiple of a nonzero vector. -/
@[simp]
theorem ray_pos_smul {v : M} (h : v ≠ 0) {r : R} (hr : 0 < r) (hrv : r • v ≠ 0) :
    rayOfNeZero R (r • v) hrv = rayOfNeZero R v h :=
  (ray_eq_iff _ _).2 <| SameRay.sameRay_pos_smul_left v hr

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