eHolderNorm_of_isEmpty — Mathlib

English

If X is empty, the Holder norm eHolderNorm r f is zero for any f.

Русский

Если множество X пусто, то норма Холдера eHolderNorm r f равна нулю для любой функции f.

LaTeX

$$$\text{IsEmpty}(X) \Rightarrow eHolderNorm(r,f) = 0$$$

Lean4

theorem eHolderNorm_of_isEmpty [hX : IsEmpty X] : eHolderNorm r f = 0 :=
  by
  rw [eHolderNorm, ← ENNReal.bot_eq_zero, iInf₂_eq_bot]
  exact fun ε hε => ⟨0, .of_isEmpty, hε⟩

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