mul_nonneg_iff_left_nonneg_of_pos

English

Let R be a linear-ordered semiring with PosMulStrictMono and MulPosStrictMono. If 0 < b, then 0 ≤ a b ↔ 0 ≤ a.

Русский

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

LaTeX

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

Lean4

theorem mul_nonneg_iff_left_nonneg_of_pos [PosMulStrictMono R] [MulPosStrictMono R] (hb : 0 < b) : 0 ≤ a * b ↔ 0 ≤ a :=
  ⟨fun h => nonneg_of_mul_nonneg_left h hb, fun h => mul_nonneg h hb.le⟩

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