mul_lt_mul_of_pos' — Mathlib

English

If a < b and c ≤ d with a > 0 and d > 0, then a·c < b·d, under the standard monotone hypotheses.

Русский

Если a < b и c ≤ d при a > 0 и d > 0, то a·c < b·d, при стандартных предпосылках монотонности.

LaTeX

$$$\\\\forall α\\,[PosMulStrictMono α][MulPosStrictMono α],\\\\\\\\forall a,b,c,d \\in α, a < b \\\\rightarrow c \\le d \\\\rightarrow 0 < a \\\\rightarrow 0 < d \\\\rightarrow a \\cdot c < b \\cdot d.$$$

Lean4

theorem mul_lt_mul_of_pos' [PosMulStrictMono α] [MulPosStrictMono α] (h₁ : a < b) (h₂ : c < d) (c0 : 0 < c)
    (b0 : 0 < b) : a * c < b * d :=
  (mul_lt_mul_of_pos_right h₁ c0).trans (mul_lt_mul_of_pos_left h₂ b0)

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