mul_nonpos_iff_pos_imp_nonpos — Mathlib

English

Under suitable order-structure, ab ≤ 0 is equivalent to (0 < a → 0 ≤ b) ∧ (b < 0 → a ≤ 0).

Русский

При надлежащей структуре порядка ab ≤ 0 эквивалентно (0 < a → b ≤ 0) и (b<0 → a ≤ 0).

LaTeX

$$$$a b \\le 0 \\iff (0 < a \\rightarrow 0 \\le b) \\land (b < 0 \\rightarrow a \\le 0).$$$$

Lean4

theorem mul_nonpos_iff_pos_imp_nonpos [PosMulStrictMono R] [MulPosStrictMono R] [AddLeftMono R] [AddLeftReflectLE R] :
    a * b ≤ 0 ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a) :=
  by
  rw [← neg_nonneg, ← mul_neg, mul_nonneg_iff_pos_imp_nonneg (R := R)]
  simp only [neg_pos, neg_nonneg]

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