sameRay_pos_smul_right — Mathlib

English

A nonnegative multiple of a vector is in the same ray as the vector.

Русский

Ненегативное кратное вектора лежит на том же луче, что и сам вектор.

LaTeX

$$sameRay_nonneg_smul_right (v) (0 ≤ a) : SameRay R v (a • v)$$

Lean4

/-- A vector is in the same ray as a positive multiple of itself. -/
theorem sameRay_pos_smul_right (v : M) (ha : 0 < a) : SameRay R v (a • v) :=
  sameRay_nonneg_smul_right v ha.le

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