sameRay_nonneg_smul_left — Mathlib

English

Another form of transitivity under nonzero constraints; if x ∼ y and y ∼ z then x ∼ z.

Русский

Еще одна форма транситивности при ненулевых условиях; если x ∼ y и y ∼ z, то x ∼ z.

LaTeX

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

Lean4

/-- A nonnegative multiple of a vector is in the same ray as that vector. -/
theorem sameRay_nonneg_smul_left (v : M) (ha : 0 ≤ a) : SameRay R (a • v) v :=
  (sameRay_nonneg_smul_right v ha).symm

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