mul_nonpos_iff_neg_imp_nonneg — Mathlib

English

Equivalent reformulations express ab ≤ 0 in terms of sign conjuncts; various equivalent forms exist under the same assumptions.

Русский

Существуют эквивалентные формулировки выражения ab ≤ 0 через знаки составляющих при тех же предпосылках.

LaTeX

$$$$0 \\le a b \\iff (a \\ge 0 \\land b \\le 0) \\lor (a \\le 0 \\land b \\ge 0).$$$$

Lean4

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

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