mul_nonneg_iff — Mathlib

English

For a,b with appropriate order properties, 0 ≤ a*b holds exactly when either a ≥ 0 and b ≥ 0 or a ≤ 0 and b ≤ 0.

Русский

Для элементов a,b с соответствующими свойствами порядка, 0 ≤ a·b существует тогда и только тогда, когда либо a ≥ 0 и b ≥ 0, либо a ≤ 0 и b ≤ 0.

LaTeX

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

Lean4

theorem mul_nonneg_iff [ExistsAddOfLE R] [MulPosStrictMono R] [PosMulStrictMono R] [AddLeftReflectLE R]
    [AddLeftMono R] : 0 ≤ a * b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 :=
  ⟨nonneg_and_nonneg_or_nonpos_and_nonpos_of_mul_nonneg, fun h =>
    h.elim (and_imp.2 mul_nonneg) (and_imp.2 mul_nonneg_of_nonpos_of_nonpos)⟩

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