le_mul_of_le_mul_of_nonneg_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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