Theorems · Theorem · functional analysis

MeasureTheory.eLpNorm_dirac

∀ {α : Type u_1} {ε : Type u_2} [inst : MeasurableSpace α] [MeasurableSingletonClass α] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {p : ENNReal} (f : α → ε) (i : α),
  p ≠ 0 → MeasureTheory.eLpNorm f p (MeasureTheory.Measure.dirac i) = ‖f i‖ₑ

Defined in

Mathlib.MeasureTheory.Function.LpSeminorm.Count

Cited by

1 results in Mathlib

Foundations

Depth 204 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceMeasurableSingletonClassTopologicalSpaceContinuousENorm