sameRay_smul_right_iff — Mathlib

English

For any v and r, SameRay(R)(v, r·v) holds iff either r≥0 or v=0, assuming NoZeroSmulDivisors.

Русский

Для любого v и r, при условии NoZeroSmulDivisors, SameRay(v, r·v) выполняется тогда и только тогда, когда r≥0 или v=0.

LaTeX

$$$\text{SameRay}(R,v, r\cdot v) \iff (0 \le r) \lor (v=0).$$$

Lean4

@[simp]
theorem sameRay_smul_right_iff {v : M} {r : R} : SameRay R v (r • v) ↔ 0 ≤ r ∨ v = 0 :=
  ⟨fun hrv => or_iff_not_imp_left.2 fun hr => eq_zero_of_sameRay_neg_smul_right (not_le.1 hr) hrv,
    or_imp.2 ⟨SameRay.sameRay_nonneg_smul_right v, fun h => h.symm ▸ SameRay.zero_left _⟩⟩

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