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)
:
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)
: