theorem MeasureTheory.Measure.measurable_of_measurable_coe' {α : Type u_1} {β : Type u_2} [MeasurableSpace β] (t : Set (Set α)) (μ : β → Measure α) [∀ (b : β), IsProbabilityMeasure (μ b)] (h : ∀ s ∈ t, Measurable fun (b : β) => (μ b) s) : Measurable μ

theorem MeasureTheory.Measure.measurable_restrict {α : Type u_1} {mα : MeasurableSpace α} {s : Set α} (hs : MeasurableSet s) : Measurable fun (μ : Measure α) => μ.restrict s

theorem MeasureTheory.Measure.measurable_setLIntegral {α : Type u_1} {mα : MeasurableSpace α} {s : Set α} {f : α → ENNReal} (hf : Measurable f) (hs : MeasurableSet s) : Measurable fun (μ : Measure α) => ∫⁻ (x : α) in s, f x ∂μ

theorem MeasureTheory.Measure.bind_null {α : Type u_1} {β : Type u_2} [MeasurableSpace β] {mα : MeasurableSpace α} {m : Measure α} {f : α → Measure β} {s : Set β} (hs : MeasurableSet s) (hf : AEMeasurable f m) : (m.bind f) s = 0 ↔ (fun (a : α) => (f a) s) =ᵐ[m] 0

theorem MeasureTheory.Measure.ae_bind_iff {α : Type u_1} {β : Type u_2} [MeasurableSpace β] {mα : MeasurableSpace α} {m : Measure α} {f : α → Measure β} {p : β → Prop} (hf : AEMeasurable f m) (hp : MeasurableSet {x : β | p x}) : (∀ᵐ (b : β) ∂m.bind f, p b) ↔ ∀ᵐ (a : α) ∂m, ∀ᵐ (b : β) ∂f a, p b