exists_pos_left_iff_sameRay_and_ne_zero

English

If x ≠ 0, then there exists r > 0 with r·x = y if and only if x and y lie on 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 \iff \operatorname{SameRay}(x,y) \land y \neq 0$ при $x \neq 0$$$

Lean4

theorem exists_pos_left_iff_sameRay_and_ne_zero (hx : x ≠ 0) : (∃ r : R, 0 < r ∧ r • x = y) ↔ SameRay R x y ∧ y ≠ 0 :=
  by
  constructor
  · rintro ⟨r, hr, rfl⟩
    simp [hx, hr.le, hr.ne']
  · rintro ⟨hxy, hy⟩
    exact (exists_pos_left_iff_sameRay hx hy).2 hxy

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