exists_nonneg_right_iff_sameRay — Mathlib

English

There exists r ≥ 0 with x = r·y if and only if x and y lie on the same ray.

Русский

Существует r ≥ 0 такое, что x = r·y тогда и только тогда, когда x и y лежат в одном луче.

LaTeX

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

Lean4

theorem exists_nonneg_right_iff_sameRay (hy : y ≠ 0) : (∃ r : R, 0 ≤ r ∧ x = r • y) ↔ SameRay R x y :=
  by
  rw [SameRay.sameRay_comm]
  simp_rw [eq_comm (a := x)]
  exact exists_nonneg_left_iff_sameRay (R := R) hy

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