nnHolderNorm_eq_zero — Mathlib

English

For a MemHolder r f, nnHolderNorm r f = 0 iff ∀ x₁ x₂, f x₁ = f x₂.

Русский

Для MemHolder r f: nnHolderNorm r f = 0 тогда и только тогда, когда ∀ x₁ x₂, f x₁ = f x₂.

LaTeX

$$$\mathrm{nnHolderNorm}(r,f) = 0 \iff \forall x_1,x_2,\ f(x_1)=f(x_2).$$$

Lean4

theorem nnHolderNorm_eq_zero {r : ℝ≥0} {f : X → Y} (hf : MemHolder r f) : nnHolderNorm r f = 0 ↔ ∀ x₁ x₂, f x₁ = f x₂ :=
  by rw [← ENNReal.coe_eq_zero, hf.coe_nnHolderNorm_eq_eHolderNorm, eHolderNorm_eq_zero]

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