sup'_mul_le_mul_sup'_of_nonneg — Mathlib

English

For a finite set s with a_i ≥ 0, b_i ≥ 0, the supremum of the product is bounded by the product of suprema: sup'_hs (a b) ≤ sup'_hs a · sup'_hs b.

Русский

Если a_i, b_i ≥ 0 для всех i∈s, то sup'_hs (a_i b_i) ≤ (sup'_hs a_i)(sup'_hs b_i).

LaTeX

$$$\sup'_{i\in s} (a_i b_i) \le (\sup'_{i\in s} a_i)(\sup'_{i\in s} b_i) \quad\text{при } a_i,b_i \ge 0.$$$

Lean4

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

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