α : Type u_1
E : Type u_2
F : Type ?u.1479555
𝕜 : Type ?u.1479558
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1482249
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
inst✝ : MeasurableSpace α
f : α → E
a : α
hfm : StronglyMeasurable f
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ (∫ (x : α), f x ∂Measure.dirac a) = f a
α : Type u_1
E : Type u_2
F : Type ?u.1479555
𝕜 : Type ?u.1479558
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1482249
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
inst✝ : MeasurableSpace α
f : α → E
a : α
hfm : StronglyMeasurable f
⊢ (∫ (x : α), f x ∂Measure.dirac a) = f a
borelize E
no goals
α : Type u_1
E : Type u_2
F : Type ?u.1479555
𝕜 : Type ?u.1479558
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1482249
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
inst✝ : MeasurableSpace α
f : α → E
a : α
hfm : StronglyMeasurable f
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ (∫ (x : α), f x ∂Measure.dirac a) = f a
calc
  (∫ x, f x ∂Measure.dirac a) = ∫ _, f a ∂Measure.dirac a :=
    integral_congr_ae <| ae_eq_dirac' hfm.measurable
  _ = f a := by simp [Measure.dirac_apply_of_mem]
no goals
α : Type u_1
E : Type u_2
F : Type ?u.1479555
𝕜 : Type ?u.1479558
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1482249
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
inst✝ : MeasurableSpace α
f : α → E
a : α
hfm : StronglyMeasurable f
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ (∫ (x : α), f a ∂Measure.dirac a) = f a
simp [Measure.dirac_apply_of_mem]