exists_nonneg_left_iff_sameRay — Mathlib

English

For x ≠ 0, the existence of a nonnegative r with r·x = y is equivalent to x and y lying on the same ray.

Русский

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

LaTeX

$$$\exists r\ge 0:\; r\cdot x = y \iff \operatorname{SameRay}(x,y)$ при $x \neq 0$$$

Lean4

theorem exists_nonneg_left_iff_sameRay (hx : x ≠ 0) : (∃ r : R, 0 ≤ r ∧ r • x = y) ↔ SameRay R x y :=
  by
  refine ⟨fun h => ?_, fun h => h.exists_nonneg_left hx⟩
  rcases h with ⟨r, hr, rfl⟩
  exact SameRay.sameRay_nonneg_smul_right x hr

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