mul_lt_mul_of_lt_of_lt — Mathlib

English

If a < b and c < d and both sides are monotone, then a*c < b*d.

Русский

Если a < b и c < d и обе стороны монотонны, то a*c < b*d.

LaTeX

$$$[\text{MulLeftStrictMono}(\alpha)]\,[\text{MulRightStrictMono}(\alpha)]\ {a,b,c,d} \; a < b \rightarrow c < d \rightarrow a\cdot c < b\cdot d.$$$

Lean4

@[to_additive (attr := gcongr high)]
theorem mul_lt_mul_of_lt_of_lt [MulLeftStrictMono α] [MulRightStrictMono α] {a b c d : α} (h₁ : a < b) (h₂ : c < d) :
    a * c < b * d :=
  calc
    a * c < a * d := mul_lt_mul_left' h₂ a
    _ < b * d := mul_lt_mul_right' h₁ d

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