English
If v1 and v2 are in the same ray, there exist nonnegative a,b with a+b=1 and a, b-scaling by a common vector u so that v1 = a·u and v2 = b·u, with u = v1+v2.
Русский
Если векторы v1 и v2 лежат в одном луче, существует общее ненулевое направление u, и неотрицательные a,b с a+b=1, такими что v1=a·u, v2=b·u, и u = v1+v2.
LaTeX
$$$\exists a,b\in\mathbb{R}_{\ge 0},\; a+b=1,\; v_1=a\,u,\; v_2=b\,u,\; u= v_1+v_2$ и при этом $\operatorname{SameRay}(v_1,v_2)$$$
Lean4
/-- If vectors `v₁` and `v₂` are on the same ray, then for some nonnegative `a b`, `a + b = 1`, we
have `v₁ = a • (v₁ + v₂)` and `v₂ = b • (v₁ + v₂)`. -/
theorem exists_eq_smul_add (h : SameRay R v₁ v₂) :
∃ a b : R, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ v₁ = a • (v₁ + v₂) ∧ v₂ = b • (v₁ + v₂) :=
by
rcases h with (rfl | rfl | ⟨r₁, r₂, h₁, h₂, H⟩)
· use 0, 1
simp
· use 1, 0
simp
· have h₁₂ : 0 < r₁ + r₂ := add_pos h₁ h₂
refine ⟨r₂ / (r₁ + r₂), r₁ / (r₁ + r₂), div_nonneg h₂.le h₁₂.le, div_nonneg h₁.le h₁₂.le, ?_, ?_, ?_⟩
· rw [← add_div, add_comm, div_self h₁₂.ne']
· rw [div_eq_inv_mul, mul_smul, smul_add, ← H, ← add_smul, add_comm r₂, inv_smul_smul₀ h₁₂.ne']
· rw [div_eq_inv_mul, mul_smul, smul_add, H, ← add_smul, add_comm r₂, inv_smul_smul₀ h₁₂.ne']
