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 ≥ 0 and d ≥ 0, then a · c ≤ b · d.

Русский

Пусть α — множество с умножением, нулем и порядком. Если a ≤ b и c ≤ d при условии a ≥ 0 и d ≥ 0, то 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) (a0 : 0 ≤ a) (d0 : 0 ≤ d) :
    a * c ≤ b * d :=
  (mul_le_mul_of_nonneg_left h₂ a0).trans (mul_le_mul_of_nonneg_right h₁ d0)

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