Mathlib Map

Theorems · Theorem · abstract harmonic analysis

MeasureTheory.Measure.dirac_conv_dirac

∀ {M : Type u_1} [inst : AddMonoid M] [inst_1 : MeasurableSpace M] [MeasurableAdd₂ M] (x y : M),
  (MeasureTheory.Measure.dirac x).conv (MeasureTheory.Measure.dirac y) = MeasureTheory.Measure.dirac (x + y)
Defined in
Mathlib.MeasureTheory.Group.Convolution
Cited by
0 results in Mathlib
Foundations
Depth 224 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
AddMonoidMeasurableSpaceMeasurableAdd₂
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

MeasurableSpace · cited by 13106MeasurableSpaceMeasureTheory.Measure · cited by 10939MeasureTheory.MeasureAddMonoid · cited by 2864AddMonoidMeasureTheory.Measure.dirac · cited by 210Measure.diracMeasurableAdd₂ · cited by 155MeasurableAdd₂measurable_id' · cited by 145measurable_id'MeasureTheory.Measure.conv · cited by 41Measure.convMeasureTheory.Measure.map_dirac' · cited by 12Measure.map_dirac'Measurable.add_const · cited by 8Measurable.add_constMeasureTheory.Measure.conv_dirac · cited by 2Measure.conv_diracMeasure.dirac_conv_diracCITED BYCITES

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.