max_mul_mul_le_max_mul_max' — Mathlib

English

For a,b,c,d in α with a monotone multiplication, the maximum of the two products is bounded by the product of the pairwise maxima: max(ab, cd) ≤ max(a,c)·max(b,d).

Русский

Для элементов a,b,c,d в упорядоченном α при монотонном умножении верно: max(ab, cd) ≤ max(a,c)·max(b,d).

LaTeX

$$$\\max(ab, cd) \leq \max(a,c) \cdot \max(b,d)$$$

Lean4

@[to_additive max_add_add_le_max_add_max]
theorem max_mul_mul_le_max_mul_max' : max (a * b) (c * d) ≤ max a c * max b d :=
  max_le (mul_le_mul' (le_max_left _ _) <| le_max_left _ _) <| mul_le_mul' (le_max_right _ _) <| le_max_right _ _

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