pi_nnnorm_const_le' — Mathlib

English

The NN-norm of the constant function a across all indices is bounded by the NN-norm of a: ‖fun i => a‖₊ ≤ ‖a‖₊.

Русский

NN-норма константной функции a по всем индексам не превосходит NN-норму a: ‖fun i => a‖₊ ≤ ‖a‖₊.

LaTeX

$$$\|\mathrm{const}_a\|_+ \le \|a\|_+$$$

Lean4

@[to_additive pi_nnnorm_const_le]
theorem pi_nnnorm_const_le' (a : E) : ‖fun _ : ι => a‖₊ ≤ ‖a‖₊ :=
  pi_norm_const_le' _

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