Theorem: SciLean.Prob.apply_measure_as_distribution (SciLean/Modules/Prob/DistribDeriv/Distribution.lean)

State before:
W : Type ?u.37841
inst✝¹² : NormedAddCommGroup W
inst✝¹¹ : NormedSpace ℝ W
inst✝¹⁰ : CompleteSpace W
X✝ : Type ?u.38068
inst✝⁹ : NormedAddCommGroup X✝
inst✝⁸ : NormedSpace ℝ X✝
inst✝⁷ : CompleteSpace X✝
Y : Type u_1
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace ℝ Y
inst✝⁴ : CompleteSpace Y
Z : Type ?u.38520
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ Z
inst✝¹ : CompleteSpace Z
X : Type u_1
inst✝ : TopologicalSpace X
μ : Measure X
φ : X → Y
⊢ ⟪↑μ, φ⟫ = ∫ (x : X), φ x ∂μ
Tactic:
rfl
State after:
no goals