mul_le_mul' — Mathlib

English

Let α be a type with multiplication and a preorder. If left multiplication is monotone and right multiplication is monotone, then for all a ≤ b and c ≤ d we have a·c ≤ b·d.

Русский

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

LaTeX

$$$$ \\forall a,b,c,d \\in \\alpha,\; a \\le b \\land c \\le d \\Rightarrow a \\cdot c \\le b \\cdot d $$$$

Lean4

@[to_additive (attr := gcongr high) add_le_add]
theorem mul_le_mul' [MulLeftMono α] [MulRightMono α] {a b c d : α} (h₁ : a ≤ b) (h₂ : c ≤ d) : a * c ≤ b * d :=
  (mul_le_mul_left' h₂ _).trans (mul_le_mul_right' h₁ d)

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