α : Type u_1
β : Type ?u.3384233
ι : Type ?u.3384236
E : Type u_2
F : Type ?u.3384242
𝕜 : Type ?u.3384245
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
p : ℝ≥0∞
μ : Measure α
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s < ⊤ → P (indicator s fun x => c)
h_closed : IsClosed {f | P ↑↑f}
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Memℒp f 1 → Memℒp g 1 → P f → P g → P (f + g)
h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → Memℒp f 1 → P f → P g
⊢ ∀ ⦃f : α → E⦄, Memℒp f 1 → P f
α : Type u_1
β : Type ?u.3384233
ι : Type ?u.3384236
E : Type u_2
F : Type ?u.3384242
𝕜 : Type ?u.3384245
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
p : ℝ≥0∞
μ : Measure α
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s < ⊤ → P (indicator s fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Integrable f → Integrable g → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → Integrable f → P f → P g
⊢ ∀ ⦃f : α → E⦄, Integrable f → P f
simp only [← memℒp_one_iff_integrable] at *
no goals
α : Type u_1
β : Type ?u.3384233
ι : Type ?u.3384236
E : Type u_2
F : Type ?u.3384242
𝕜 : Type ?u.3384245
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
p : ℝ≥0∞
μ : Measure α
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s < ⊤ → P (indicator s fun x => c)
h_closed : IsClosed {f | P ↑↑f}
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Memℒp f 1 → Memℒp g 1 → P f → P g → P (f + g)
h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → Memℒp f 1 → P f → P g
⊢ ∀ ⦃f : α → E⦄, Memℒp f 1 → P f
exact Memℒp.induction one_ne_top (P := P) h_ind h_add h_closed h_ae