sup_mul_le_mul_sup_of_nonneg — Mathlib

English

For a finite index set s and nonnegative arrays a_i, b_i, the supremum of the pointwise products is bounded by the product of the suprema: sup_i (a_i b_i) ≤ (sup_i a_i)(sup_i b_i).

Русский

Для конечного множества индексов s и неотрицательных последовательностей a_i, b_i имеем: sup_i (a_i b_i) ≤ (sup_i a_i)(sup_i b_i).

LaTeX

$$$\sup_{i\in s} (a_i b_i) \le \left(\sup_{i\in s} a_i\right)\left(\sup_{i\in s} b_i\right),\quad a_i,b_i\ge 0.$$$

Lean4

theorem sup_mul_le_mul_sup_of_nonneg [SemilatticeSup M₀] [OrderBot M₀] [PosMulMono M₀] [MulPosMono M₀]
    (ha : ∀ i ∈ s, 0 ≤ a i) (hb : ∀ i ∈ s, 0 ≤ b i) : s.sup (a * b) ≤ s.sup a * s.sup b :=
  Finset.sup_le fun _i hi ↦ mul_le_mul (le_sup hi) (le_sup hi) (hb _ hi) ((ha _ hi).trans <| le_sup hi)

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