nonneg_of_mul_nonneg_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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