mul_le_of_mul_le_of_nonneg_left — Mathlib

English

Let α be a type with a multiplication, a zero, and a preorder, equipped with the property that left multiplication by a nonnegative element is order-preserving. If a, b, c, d ∈ α satisfy a*b ≤ c, d ≤ b, and 0 ≤ a, then a*d ≤ c.

Русский

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

LaTeX

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

Lean4

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

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