nonpos_of_mul_nonpos_right — Mathlib

English

Let R be a semiring with a linear order and PosMulStrictMono. If a b ≤ 0 and 0 < a, then b ≤ 0.

Русский

Пусть R — полукольцо с линейным порядком и PosMulStrictMono. Если a b ≤ 0 и 0 < a, то b ≤ 0.

LaTeX

$$$\\forall a,b\\in R\\, (a b \\le 0) \\land (0 < a) \\Rightarrow b \\le 0$$$

Lean4

theorem nonpos_of_mul_nonpos_right [PosMulStrictMono R] (h : a * b ≤ 0) (ha : 0 < a) : b ≤ 0 :=
  le_of_not_gt fun hb : b > 0 => (mul_pos ha hb).not_ge h

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