mul_lt_mul_of_le_of_lt_of_pos_of_nonneg

English

If a ≤ b and c < d with a ≥ 0 and d ≥ 0, then a · c < b · d, assuming the monotonicity and positivity conditions.

Русский

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

LaTeX

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

Lean4

theorem mul_lt_mul_of_le_of_lt_of_pos_of_nonneg [PosMulStrictMono α] [MulPosMono α] (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_le (mul_le_mul_of_nonneg_right h₁ d0)

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