smul_pos_iff_of_pos_left — Mathlib

English

If a > 0, then a • b < 0 if and only if b < 0.

Русский

Если a > 0, то a • b < 0 тогда и только тогда, когда b < 0.

LaTeX

$$[PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : 0 < a) : a • b < 0 \\iff b < 0$$

Lean4

@[simp]
theorem smul_pos_iff_of_pos_left [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : 0 < a) : 0 < a • b ↔ 0 < b := by
  simpa only [smul_zero] using smul_lt_smul_iff_of_pos_left ha (b₁ := 0) (b₂ := b)

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