pos_smul_left — Mathlib

English

If x and y lie on the same ray, then for any positive scalar a, a·x and y lie on the same ray.

Русский

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

LaTeX

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

Lean4

/-- A positive multiple of a vector is in the same ray as one it is in the same ray as. -/
theorem pos_smul_left (h : SameRay R x y) (hr : 0 < a) : SameRay R (a • x) y :=
  h.nonneg_smul_left hr.le

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