mul_le_mul_three — Mathlib

English

If left multiplication is monotone and right multiplication is monotone, and a ≤ d, b ≤ e, c ≤ f, then a·b·c ≤ d·e·f.

Русский

Если левая и правая умножения монотонны и a ≤ d, b ≤ e, c ≤ f, то a·b·c ≤ d·e·f.

LaTeX

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

Lean4

@[to_additive]
theorem mul_le_mul_three [MulLeftMono α] [MulRightMono α] {a b c d e f : α} (h₁ : a ≤ d) (h₂ : b ≤ e) (h₃ : c ≤ f) :
    a * b * c ≤ d * e * f :=
  mul_le_mul' (mul_le_mul' h₁ h₂) h₃

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