English
If two vectors v1 and v2 are on the same ray, there exist nonnegative a,b and a vector u such that v1 = a·u, v2 = b·u and a+b=1.
Русский
Если векторы v1 и v2 лежат на одном луче, существует ненулевые коэффициенты a,b ≥ 0 и общий вектор u, такой что v1=a·u, v2=b·u и a+b=1.
LaTeX
$$$\exists a,b\in\mathbb{R}_{\ge 0},\; a+b=1,\; \exists u:\; v_1=a\,u,\; v_2=b\,u$$$
Lean4
/-- If vectors `v₁` and `v₂` are on the same ray, then they are nonnegative multiples of the same
vector. Actually, this vector can be assumed to be `v₁ + v₂`, see `SameRay.exists_eq_smul_add`. -/
theorem exists_eq_smul (h : SameRay R v₁ v₂) :
∃ (u : M) (a b : R), 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ v₁ = a • u ∧ v₂ = b • u :=
⟨v₁ + v₂, h.exists_eq_smul_add⟩
