mul_neg_iff — Mathlib

English

For a,b ∈ EReal, a*b < 0 iff (0 < a ∧ b < 0) ∨ (a < 0 ∧ 0 < b).

Русский

Для a,b ∈ EReal произведение a*b отрицательно тогда и только тогда, когда один из множителей положителен, другой отрицателен.

LaTeX

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

Lean4

theorem mul_neg_iff {a b : EReal} : a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b :=
  by
  nth_rw 1 [← neg_zero]
  rw [lt_neg_comm, ← mul_neg a, mul_pos_iff, neg_lt_comm, lt_neg_comm, neg_zero]

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