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 PosMulStrictMono and MulPosStrictMono.

Русский

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

LaTeX

$$$\\\\forall α\\,[PosMulStrictMono α][MulPosStrictMono α],\\\\\\\\forall a,b,c,d \\in α, a < b \\\\rightarrow c < 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) (a0 : 0 < a)
    (d0 : 0 < d) : a * c < b * d :=
  (mul_lt_mul_of_pos_left h₂ a0).trans (mul_lt_mul_of_pos_right h₁ d0)

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