eLpNormEssSup_measure_zero — Mathlib

English

The essential supremum norm of a constant function c is equal to the norm of c, i.e., eLpNormEssSup c μ = ∥c∥ₑ, provided μ is nonzero.

Русский

Эссенциальная верхняя граница нормы константной функции c равна норме c: eLpNormEssSup c μ = ∥c∥ₑ при μ ≠ 0.

LaTeX

$$$eLpNormEssSup (\\lambda x. c) \\mu = \\|c\\|_e$$$

Lean4

@[simp]
theorem eLpNormEssSup_measure_zero {f : α → ε} : eLpNormEssSup f (0 : Measure α) = 0 := by simp [eLpNormEssSup]

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