mul_nonneg_of_nonneg_or_nonpos — Mathlib

English

For integers a and b, 0 ≤ a b if and only if either both a and b are nonnegative or both are nonpositive.

Русский

Для целых чисел a и b having 0 ≤ ab тогда и только тогда, когда либо оба неотрицательны, либо оба неположительны.

LaTeX

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

Lean4

theorem mul_nonneg_of_nonneg_or_nonpos {a b : ℤ} : 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 → 0 ≤ a * b
  | .inl ⟨ha, hb⟩ => Int.mul_nonneg ha hb
  | .inr ⟨ha, hb⟩ => Int.mul_nonneg_of_nonpos_of_nonpos ha hb

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