α : Type u_1
β : Type u_2
γ : Type ?u.1262382
δ : Type ?u.1262385
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hf : AEStronglyMeasurable f μ
⊢ MeasureTheory.Integrable ↑(mk f hf) ↔ MeasureTheory.Integrable f
α : Type u_1
β : Type u_2
γ : Type ?u.1262382
δ : Type ?u.1262385
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hf : AEStronglyMeasurable f μ
⊢ Integrable (mk f hf) ↔ MeasureTheory.Integrable f
simp [Integrable]
case h
α : Type u_1
β : Type u_2
γ : Type ?u.1262382
δ : Type ?u.1262385
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hf : AEStronglyMeasurable f μ
⊢ ↑(mk f hf) =ᵐ[μ] f
α : Type u_1
β : Type u_2
γ : Type ?u.1262382
δ : Type ?u.1262385
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hf : AEStronglyMeasurable f μ
⊢ MeasureTheory.Integrable ↑(mk f hf) ↔ MeasureTheory.Integrable f
apply integrable_congr
no goals
case h
α : Type u_1
β : Type u_2
γ : Type ?u.1262382
δ : Type ?u.1262385
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hf : AEStronglyMeasurable f μ
⊢ ↑(mk f hf) =ᵐ[μ] f
exact coeFn_mk f hf