exists_pos_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem exists_pos_left (h : SameRay R x y) (hx : x ≠ 0) (hy : y ≠ 0) : ∃ r : R, 0 < r ∧ r • x = y :=
  let ⟨r₁, r₂, hr₁, hr₂, h⟩ := h.exists_pos hx hy
  ⟨r₂⁻¹ * r₁, mul_pos (inv_pos.2 hr₂) hr₁, by rw [mul_smul, h, inv_smul_smul₀ hr₂.ne']⟩

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