exists_pos — Mathlib

English

If x is on the same ray as y and y is on the same ray as z, and certain nonzero conditions hold, then x is on the same ray as z.

Русский

Если x на том же луче, что и y, и y на том же луче, что и z, и учитываются условия ненулевых, тогда x на том же луче, что и z.

LaTeX

$$trans (hxy) (hyz) (hy) : SameRay R x z$$

Lean4

/-- If `x` and `y` are nonzero vectors on the same ray, then there exist positive numbers `r₁ r₂`
such that `r₁ • x = r₂ • y`. -/
theorem exists_pos (h : SameRay R x y) (hx : x ≠ 0) (hy : y ≠ 0) : ∃ r₁ r₂ : R, 0 < r₁ ∧ 0 < r₂ ∧ r₁ • x = r₂ • y :=
  (h.resolve_left hx).resolve_left hy

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