pos_smul_right — Mathlib

English

If x and y lie on the same ray, then for any positive 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 < a \;\Rightarrow\; \operatorname{SameRay}(R, x, a \cdot y). $$$

Lean4

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

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