mul_nonneg_iff — Mathlib

English

If a and b are nonnegative, then their product a·b is nonnegative.

Русский

Если a и b неотрицательны, то их произведение неотрицательно.

LaTeX

$$$a \ge 0 \land b \ge 0 \Rightarrow a b \ge 0$$$

Lean4

theorem mul_nonneg_iff {a b : EReal} : 0 ≤ a * b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 :=
  by
  simp_rw [le_iff_lt_or_eq, mul_pos_iff, zero_eq_mul (a := a)]
  rcases lt_trichotomy a 0 with (h | h | h) <;> rcases lt_trichotomy b 0 with (h' | h' | h') <;>
      simp only [h, h', true_or, true_and, or_true, and_true] <;>
    tauto

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