div_nonneg_iff — Mathlib

English

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

Русский

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

LaTeX

$$$0 \le \dfrac{a}{b} \iff (0 \le a \land 0 \le b) \lor (a \le 0 \land b \le 0)$$$

Lean4

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

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