nonneg_smul_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- A vector is in the same ray as a nonnegative multiple of one it is in the same ray as. -/
theorem nonneg_smul_right (h : SameRay R x y) (ha : 0 ≤ a) : SameRay R x (a • y) :=
  h.trans (sameRay_nonneg_smul_right y ha) fun hy => Or.inr <| by rw [hy, smul_zero]

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