mul_nonneg_iff_of_pos_right — Mathlib

English

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

Русский

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

LaTeX

$$$0 < c \Rightarrow (0 \le b c \iff 0 \le b)$$$

Lean4

@[simp]
theorem mul_nonneg_iff_of_pos_right [MulPosStrictMono R] (h : 0 < c) : 0 ≤ b * c ↔ 0 ≤ b := by
  simpa using (mul_le_mul_iff_left₀ h : 0 * c ≤ b * c ↔ 0 ≤ b)

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