mul_le_mul_of_nonneg' — Mathlib

English

Let α be a type with multiplication, zero, and a preorder. If a ≤ b and c ≤ d with a,b,c,d ≥ 0, then a · c ≤ b · d.

Русский

Пусть α — множество с умножением, нулем и порядком. Если a ≤ b и c ≤ d и все a,b,c,d неотрицательны, то a · c ≤ b · d.

LaTeX

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

Lean4

theorem mul_le_mul_of_nonneg' [PosMulMono α] [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 (mul_le_mul_of_nonneg_left h₂ b0)

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