exists_pos_left_iff_sameRay — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem exists_pos_left_iff_sameRay (hx : x ≠ 0) (hy : y ≠ 0) : (∃ r : R, 0 < r ∧ r • x = y) ↔ SameRay R x y :=
  by
  refine ⟨fun h => ?_, fun h => h.exists_pos_left hx hy⟩
  rcases h with ⟨r, hr, rfl⟩
  exact SameRay.sameRay_pos_smul_right x hr

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