Theorems · Theorem · measure theory

MeasureTheory.Measure.sum_smul_dirac_singleton

∀ {α : Type u_1} [inst : MeasurableSpace α] [MeasurableSingletonClass α] {f : α → ENNReal} {a : α},
  (MeasureTheory.Measure.sum fun b => f b • MeasureTheory.Measure.dirac b) {a} = f a

The sum of scaled Dirac measures applied to a singleton is the coefficient of that singleton.

Defined in

Mathlib.MeasureTheory.Measure.Dirac

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSingletonClass