∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {f : α → E} [MeasureTheory.IsProbabilityMeasure μ],
  Convex ℝ s → IsClosed s → (∀ᵐ (x : α) ∂μ, f x ∈ s) → MeasureTheory.Integrable f μ → ∫ (x : α), f x ∂μ ∈ s