min_mul_min_le_min_mul_mul' — Mathlib

English

For α with monotone multiplication, the product of minima is bounded above by the minimum of the products: min(a,c)·min(b,d) ≤ min(ab, cd).

Русский

Для упорядоченного α с монотонным умножением произведение минимумов не превосходит минимум произведений: min(a,c)·min(b,d) ≤ min(ab, cd).

LaTeX

$$$\\min(a,c)\\cdot\\min(b,d) \\le \\min(ab, cd)$$$

Lean4

@[to_additive min_add_min_le_min_add_add]
theorem min_mul_min_le_min_mul_mul' : min a c * min b d ≤ min (a * b) (c * d) :=
  le_min (mul_le_mul' (min_le_left _ _) <| min_le_left _ _) <| mul_le_mul' (min_le_right _ _) <| min_le_right _ _

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