mul_lt_mul'' — Mathlib

English

If a < c and b < d with a,b ≥ 0 and certain monotonicity conditions, then a b < c d.

Русский

Если a < c и b < d при a,b ≥ 0 и соответствующих монотонных условиях, то a b < c d.

LaTeX

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

Lean4

protected theorem mul_lt_mul'' [PosMulMono M₀] [PosMulStrictMono M₀] [MulPosStrictMono M₀] [DecidableLE M₀] (h1 : a < c)
    (h2 : b < d) (h3 : 0 ≤ a) (h4 : 0 ≤ b) : a * b < c * d :=
  h4.lt_or_eq_dec.elim (fun b0 ↦ mul_lt_mul h1 h2.le b0 <| h3.trans h1.le) fun b0 ↦ by rw [← b0, mul_zero];
    exact mul_pos (h3.trans_lt h1) (h4.trans_lt h2)

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