coe_nnHolderNorm_le_eHolderNorm — Mathlib

English

The nonnegative real Holder norm is bounded above by the Holder norm: (nnHolderNorm r f : ℝ≥0∞) ≤ eHolderNorm r f.

Русский

Нормa Холдера в неотрицательном формате не превосходит норму Холдера: (nnHolderNorm r f : ℝ≥0∞) ≤ eHolderNorm r f.

LaTeX

$$$\bigl(\mathrm{nnHolderNorm}(r,f)\bigr) : \mathbb{R}_{\ge 0}^{\infty} \le eHolderNorm(r,f).$$$

Lean4

theorem coe_nnHolderNorm_le_eHolderNorm {r : ℝ≥0} {f : X → Y} : (nnHolderNorm r f : ℝ≥0∞) ≤ eHolderNorm r f :=
  coe_toNNReal_le_self

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