mul_lt_mul_of_le_of_lt_of_nonneg_of_pos

English

If a ≤ b and c < d with a ≥ 0 and d > 0, then a · c < b · d, under the usual monotonicity assumptions.

Русский

Если a ≤ b и c < d при условии a ≥ 0 и d > 0, тогда a · c < b · d, при обычных предположениях монотонности.

LaTeX

$$$\\\\forall α\\,[PosMulMono\\;α][MulPosMono\\;α],\\\\\\\\forall a,b,c,d \\in α, a \\le b \\rightarrow c < d \\rightarrow 0 \\le a \\rightarrow 0 < d \\rightarrow a \\cdot c < b \\cdot d.$$$

Lean4

theorem mul_lt_mul_of_le_of_lt_of_nonneg_of_pos [PosMulStrictMono α] [MulPosMono α] (h₁ : a ≤ b) (h₂ : c < d)
    (c0 : 0 ≤ c) (b0 : 0 < b) : a * c < b * d :=
  (mul_le_mul_of_nonneg_right h₁ c0).trans_lt (mul_lt_mul_of_pos_left h₂ b0)

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