mul_nonpos_iff — Mathlib

English

For a ring with appropriate monotonicity, ab ≤ 0 is equivalent to either a ≥ 0 and b ≤ 0, or a ≤ 0 and b ≥ 0.

Русский

Для кольца с подходящей монотонностью равносильно тому, что произведение неотрицательно тогда и только тогда, когда знаки коэффициентов противоположны.

LaTeX

$$$$a b \\le 0 \\;\\Leftrightarrow\\; (0 \\le a \\land b \\le 0) \\lor (a \\le 0 \\land 0 \\le b).$$$$

Lean4

theorem mul_nonpos_iff [MulPosStrictMono R] [PosMulStrictMono R] [AddLeftReflectLE R] [AddLeftMono R] :
    a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b := by
  rw [← neg_nonneg, neg_mul_eq_mul_neg, mul_nonneg_iff (R := R), neg_nonneg, neg_nonpos]

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