theorem MeasureTheory.Integrable.induction' {α : Type u_1} {E : Type u_2} {mα : MeasurableSpace α} [NormedAddCommGroup E] {μ : Measure α} (P : (f : α → E) → Integrable f μ → Prop) (indicator : ∀ (c : E) (s : Set α) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤), P (s.indicator fun (x : α) => c) ⋯) (add : ∀ (f g : α → E) (hf : Integrable f μ) (hg : Integrable g μ), Disjoint (Function.support f) (Function.support g) → P f hf → P g hg → P (f + g) ⋯) (isClosed : IsClosed {f : ↥(Lp E 1 μ) | P ↑↑f ⋯}) (ae_congr : ∀ (f g : α → E) (hf : Integrable f μ) (hfg : f =ᶠ[ae μ] g), P f hf → P g ⋯) (f : α → E) (hf : Integrable f μ) : P f hf

theorem MeasureTheory.SimpleFunc.integrable_of_isFiniteMeasure' {α : Type u_1} {E : Type u_2} {mα : MeasurableSpace α} [NormedAddCommGroup E] {μ : Measure α} {mα₀ : MeasurableSpace α} (hα : mα₀ ≤ mα) [IsFiniteMeasure μ] (f : SimpleFunc α E) : Integrable (⇑f) μ