mul_lt_of_mul_lt_of_nonneg_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem mul_lt_of_mul_lt_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_lt h

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