nnHolderNorm_const — Mathlib

English

The NNHolderNorm of the zero function is zero: nnHolderNorm r (0 : X → Y) = 0.

Русский

NNHolderNorm нуля функции равен нулю: nnHolderNorm r (0 : X → Y) = 0.

LaTeX

$$$\mathrm{nnHolderNorm}(r,0) = 0.$$$

Lean4

@[simp]
theorem nnHolderNorm_const (r : ℝ≥0) (c : Y) : nnHolderNorm r (Function.const X c) = 0 :=
  by
  refine le_antisymm (ENNReal.coe_le_coe.1 <| le_trans coe_nnHolderNorm_le_eHolderNorm ?_) (zero_le _)
  rw [eHolderNorm_const, ENNReal.coe_zero]

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