α : Type u_2
β✝ : Type ?u.954430
γ : Type ?u.954433
δ : Type ?u.954436
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β✝
inst✝¹ : NormedAddCommGroup γ
β : Type u_1
inst✝ : NormedLatticeAddCommGroup β
f g : α → β
hf : Memℒp f 1
hg : Memℒp g 1
⊢ Memℒp (f ⊔ g) 1
α : Type u_2
β✝ : Type ?u.954430
γ : Type ?u.954433
δ : Type ?u.954436
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β✝
inst✝¹ : NormedAddCommGroup γ
β : Type u_1
inst✝ : NormedLatticeAddCommGroup β
f g : α → β
hf : Integrable f
hg : Integrable g
⊢ Integrable (f ⊔ g)
rw [← memℒp_one_iff_integrable] at hf hg⊢
no goals
α : Type u_2
β✝ : Type ?u.954430
γ : Type ?u.954433
δ : Type ?u.954436
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β✝
inst✝¹ : NormedAddCommGroup γ
β : Type u_1
inst✝ : NormedLatticeAddCommGroup β
f g : α → β
hf : Memℒp f 1
hg : Memℒp g 1
⊢ Memℒp (f ⊔ g) 1
exact hf.sup hg