mul_lt_of_mul_lt_of_nonneg_right — Mathlib

English

Let α be a type with multiplication, a zero, and a preorder, with MulPosMono. If a*b < c, d ≤ a, and 0 ≤ b, then d*b < c.

Русский

Пусть α — множество с умножением, нулём и порядком; если a·b < c, d ≤ a, и 0 ≤ b, тогда d·b < c.

LaTeX

$$$\forall a,b,c,d \in \alpha,\ a b < c,\ d \le a,\ 0 \le b \Rightarrow d b < c$$$

Lean4

theorem mul_lt_of_mul_lt_of_nonneg_right [MulPosMono α] (h : a * b < c) (hle : d ≤ a) (b0 : 0 ≤ b) : d * b < c :=
  (mul_le_mul_of_nonneg_right hle b0).trans_lt h

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