smul_nonpos_iff_pos_imp_nonpos — Mathlib

English

0 ≤ a·b iff 0 ≤ a and 0 ≤ b or a ≤ 0 and b ≤ 0.

Русский

0 ≤ a·b тогда и только тогда, когда либо 0 ≤ a и 0 ≤ b, либо a ≤ 0 и b ≤ 0.

LaTeX

$$$0 \le a \cdot b \iff (0 \le a \land 0 \le b) \lor (a \le 0 \land b \le 0)$$$

Lean4

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

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