exists_pos_right_iff_sameRay — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem exists_pos_right_iff_sameRay (hx : x ≠ 0) (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_pos_left_iff_sameRay hy hx

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