exists_nonneg_right — Mathlib

English

If y ≠ 0 and x is in the same ray as y, there exists r ≥ 0 with x = r·y.

Русский

Если y ≠ 0 и x лежит в том же луче, то существует r ≥ 0 such that x = r·y.

LaTeX

$$$\exists r\ge 0:\; x = r\cdot y \quad\text{iff}\quad \operatorname{SameRay}(x,y) \land y \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_right (h : SameRay R x y) (hy : y ≠ 0) : ∃ r : R, 0 ≤ r ∧ x = r • y :=
  (h.symm.exists_nonneg_left hy).imp fun _ => And.imp_right Eq.symm

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