le_mul_of_le_mul_of_nonneg_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem le_mul_of_le_mul_of_nonneg_right [MulPosMono α] (h : a ≤ b * c) (hle : b ≤ d) (c0 : 0 ≤ c) : a ≤ d * c :=
  h.trans (mul_le_mul_of_nonneg_right hle c0)

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