smul_nonpos_iff_neg_imp_nonneg — Mathlib

English

Let a be a scalar from a linearly ordered ring and b an element from a linearly ordered module with a compatible scalar action. Then a • b ≤ 0 holds exactly when (a < 0 implies 0 ≤ b) and (0 < b implies a ≤ 0).

Русский

Пусть a — скаляр из упорядоченного кольца и b — элемент модуля с совместимым скалярным действием. Тогда a • b ≤ 0 тогда и только тогда, когда (a < 0 означает 0 ≤ b) и (0 < b означает a ≤ 0).

LaTeX

$$$a \cdot b \le 0 \iff (a<0 \to 0 \le b) \land (0 < b \to a \le 0)$$$

Lean4

theorem smul_nonpos_iff_neg_imp_nonneg : a • b ≤ 0 ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0) := by
  rw [← neg_nonneg, ← neg_smul, smul_nonneg_iff_pos_imp_nonneg]; simp only [neg_pos, neg_nonneg]

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