lt_mul_of_lt_mul_of_nonneg_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem lt_mul_of_lt_mul_of_nonneg_left [PosMulMono α] (h : a < b * c) (hle : c ≤ d) (b0 : 0 ≤ b) : a < b * d :=
  h.trans_le (mul_le_mul_of_nonneg_left hle b0)

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