mul_nonneg_iff — Mathlib

English

Equivalence: 0 ≤ a b is equivalent to (0 ≤ a ∧ 0 ≤ b) ∨ (a ≤ 0 ∧ b ≤ 0).

Русский

Эквивалентность: 0 ≤ a b эквивалентно (0 ≤ a ∧ 0 ≤ b) ∨ (a ≤ 0 ∧ b ≤ 0).

LaTeX

$$$\forall {a,b : \mathbb{Z}}, 0 \le a b \iff (0 \le a \land 0 \le b) \lor (a \le 0 \land b \le 0).$$$

Lean4

protected theorem mul_nonneg_iff {a b : ℤ} : 0 ≤ a * b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 :=
  ⟨nonneg_or_nonpos_of_mul_nonneg, mul_nonneg_of_nonneg_or_nonpos⟩

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