exists_pos_right_iff_sameRay_and_ne_zero

English

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

Русский

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

LaTeX

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

Lean4

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

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