LeanPool.ZhangYeungInequality.PFR.Mathlib.MeasureTheory.Measure.Dirac #
Imported Lean Pool material for
LeanPool.ZhangYeungInequality.PFR.Mathlib.MeasureTheory.Measure.Dirac.
@[simp]
theorem
MeasureTheory.Measure.dirac_real_apply'
{α : Type u_1}
[MeasurableSpace α]
{s : Set α}
(a : α)
(hs : MeasurableSet s)
: