nonneg_smul_left — Mathlib

English

If two vectors x and y are on the same ray, then for any nonnegative scalar a, a·x and y are on the same ray.

Русский

Если x и y лежат на одном луче, то для любого неотрицательного a вектор a·x и y лежат на одном луче.

LaTeX

$$$ \operatorname{SameRay}(R, x, y) \;\Rightarrow\; 0 \le a \;\Rightarrow\; \operatorname{SameRay}(R, a \cdot x, y). $$$

Lean4

/-- A nonnegative multiple of a vector is in the same ray as one it is in the same ray as. -/
theorem nonneg_smul_left (h : SameRay R x y) (ha : 0 ≤ a) : SameRay R (a • x) y :=
  (h.symm.nonneg_smul_right ha).symm

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