bind_apply — Mathlib

English

For measurable s and AEMeasurable f, bind m f s = ∫ f a s ∂m.

Русский

Для измеримого s и AEMeasurable f выполняется bind m f s = ∫ f a s ∂m.

LaTeX

$$$\\text{bind } m\\ f\\ s = \\int⁻ a, f a\\, s \\, \\partial m$$$

Lean4

@[simp]
theorem bind_apply {m : Measure α} {f : α → Measure β} {s : Set β} (hs : MeasurableSet s) (hf : AEMeasurable f m) :
    bind m f s = ∫⁻ a, f a s ∂m := by rw [bind, join_apply hs, lintegral_map' (measurable_coe hs).aemeasurable hf]

Похожие утверждения