nnnorm_tprod_le — Mathlib

English

In the NNReal-augmented setting, the nonnegative norm of the tprod is bounded by the supremum of the nonnegative norms: ‖∏' i, f i‖₊ ≤ sup_i ‖f i‖₊.

Русский

В настройке с NNReal неотрицательная норма tprod не превосходит супремума негатива: ‖∏' i, f i‖₊ ≤ sup_i ‖f i‖₊.

LaTeX

$$$\\|\\prod' i, f(i)\\|_+ \\le \\sup_i \\|f(i)\\|_+$$

Lean4

@[to_additive]
theorem nnnorm_tprod_le (f : ι → M) : ‖∏' i, f i‖₊ ≤ ⨆ i, ‖f i‖₊ := by
  simpa only [← NNReal.coe_le_coe, coe_nnnorm', coe_iSup] using norm_tprod_le f

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