mul_neg_iff — Mathlib

English

In a linearly ordered ring with appropriate monotonicity, ab < 0 holds exactly when a and b have opposite signs: either a > 0 and b < 0, or a < 0 and b > 0.

Русский

В упорядоченном кольце с требуемыми свойствами произведение двух элементов отрицательно тогда и только тогда их знаки противоположны.

LaTeX

$$$$a b < 0 \;\;\\Longleftrightarrow\\; (0 < a \\land b < 0) \\lor (a < 0 \\land 0 < b).$$$$

Lean4

theorem mul_neg_iff [PosMulStrictMono R] [MulPosStrictMono R] [AddLeftReflectLT R] [AddLeftStrictMono R] :
    a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b := by
  rw [← neg_pos, neg_mul_eq_mul_neg, mul_pos_iff (R := R), neg_pos, neg_lt_zero]

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