nonpos_of_mul_nonpos_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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