div_nonpos_iff — Mathlib

English

For a linearly ordered field α, a/b ≤ 0 if and only if (0 ≤ a and b ≤ 0) or (a ≤ 0 and 0 ≤ b).

Русский

Пусть α — упорядоченное поле; тогда a/b ≤ 0 тогда и только тогда, когда (a ≥ 0 и b ≤ 0) или (a ≤ 0 и b ≥ 0).

LaTeX

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

Lean4

theorem div_nonpos_iff : a / b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b := by simp [division_def, mul_nonpos_iff]

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