div_neg_iff — Mathlib

English

In a linearly ordered field α, a/b is negative if and only if exactly one of a,b is positive and the other is negative; equivalently (0 < a and b < 0) or (a < 0 and 0 < b).

Русский

Пусть α — упорядоченное поле; тогда a/b < 0 тогда и только тогда, когда один из a,b положителен, а другой отрицателен; эквивалентно (0 < a ∧ b < 0) или (a < 0 ∧ 0 < b).

LaTeX

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

Lean4

theorem div_neg_iff : a / b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b := by simp [division_def, mul_neg_iff]

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