mul_nonneg_iff_neg_imp_nonpos — Mathlib

English

In a linearly ordered ring with the stated monotonicity, 0 ≤ a b is equivalent to (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0).

Русский

Для упорядоченного кольца при соответствующей монотонности неравенство 0 ≤ ab эквивалентно условию, что если a < 0, то b ≤ 0, и если b < 0, то a ≤ 0.

LaTeX

$$$$0 \\le a b \\iff (a < 0 \\rightarrow b \\le 0) \\land (b < 0 \\rightarrow a \\le 0).$$$$

Lean4

theorem mul_nonneg_iff_neg_imp_nonpos [PosMulStrictMono R] [MulPosStrictMono R] [AddLeftMono R] [AddLeftReflectLE R] :
    0 ≤ a * b ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0) := by rw [← neg_mul_neg, mul_nonneg_iff_pos_imp_nonneg (R := R)];
  simp only [neg_pos, neg_nonneg]

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