coe_nnHolderNorm_eq_eHolderNorm — Mathlib

English

If f is a MemHolder r f, then ENNReal.ofNNReal(nnHolderNorm r f) = eHolderNorm r f.

Русский

Если f является MemHolder r f, то ENNReal.ofNNReal(nnHolder r f) = eHolderNorm r f.

LaTeX

$$$\mathrm{ENNReal.ofNNReal}(\mathrm{nnHolderNorm}(r,f)) = eHolderNorm(r,f).$$$

Lean4

theorem coe_nnHolderNorm_eq_eHolderNorm {r : ℝ≥0} {f : X → Y} (hf : MemHolder r f) :
    (nnHolderNorm r f : ℝ≥0∞) = eHolderNorm r f :=
  by
  rw [nnHolderNorm, coe_toNNReal]
  exact ne_of_lt <| lt_of_le_of_lt hf.holderWith.eHolderNorm_le <| coe_lt_top

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