exists_nonneg_left — Mathlib

English

If x and y are in the same ray and x ≠ 0, there exists a nonnegative scalar r with r·x = y.

Русский

Если x и y лежат в одном луче и x ≠ 0, существует неотрицательный скаляр r такой, что r·x = y.

LaTeX

$$$\exists r\ge 0:\; r\cdot x = y \quad\text{given } \operatorname{SameRay}(x,y) \land x \neq 0$$$

Lean4

/-- If a vector `v₂` is on the same ray as a nonzero vector `v₁`, then it is equal to `c • v₁` for
some nonnegative `c`. -/
theorem exists_nonneg_left (h : SameRay R x y) (hx : x ≠ 0) : ∃ r : R, 0 ≤ r ∧ r • x = y :=
  by
  obtain rfl | hy := eq_or_ne y 0
  · exact ⟨0, le_rfl, zero_smul _ _⟩
  · exact (h.exists_pos_left hx hy).imp fun _ => And.imp_left le_of_lt

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