mul_le_of_mul_le_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 \le c,\ d \le a,\ 0 \le b \Rightarrow d b \le c$$$

Lean4

theorem mul_le_of_mul_le_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 h

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