exists_pos_right — Mathlib

English

If x ≠ 0, then there exists r > 0 with r·x = y if and only if x and y are in the same ray and y ≠ 0.

Русский

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

LaTeX

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

Lean4

theorem exists_pos_right (h : SameRay R x y) (hx : x ≠ 0) (hy : y ≠ 0) : ∃ r : R, 0 < r ∧ x = r • y :=
  (h.symm.exists_pos_left hy hx).imp fun _ => And.imp_right Eq.symm

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