mul_lt_mul_of_nonneg — Mathlib

English

If a < b and c < d and a ≥ 0 and c ≥ 0, then a c < b d.

Русский

Если a < b и c < d и a ≥ 0 и c ≥ 0, тогда a c < b d.

LaTeX

$$$$ a < b \land c < d \land a \ge 0 \land c \ge 0 \Rightarrow a c < b d. $$$$

Lean4

/-- Assumes left strict covariance. -/
theorem mul_lt_mul_of_nonneg [PosMulStrictMono α] [MulPosMono α] (h₁ : a < b) (h₂ : c < d) (a0 : 0 ≤ a) (c0 : 0 ≤ c) :
    a * c < b * d :=
  mul_lt_mul_of_le_of_lt_of_nonneg_of_pos h₁.le h₂ c0 (a0.trans_lt h₁)

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