α : Type u_1
β : Type u_2
γ : Type ?u.718349
δ : Type ?u.718352
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hμ : (∫⁻ (a : α), ↑‖f a‖₊ ∂μ) < ⊤
hν : (∫⁻ (a : α), ↑‖f a‖₊ ∂ν) < ⊤
⊢ ((∫⁻ (a : α), ↑‖f a‖₊ ∂μ) + ∫⁻ (a : α), ↑‖f a‖₊ ∂ν) < ⊤
α : Type u_1
β : Type u_2
γ : Type ?u.718349
δ : Type ?u.718352
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hμ : HasFiniteIntegral f
hν : HasFiniteIntegral f
⊢ HasFiniteIntegral f
simp only [HasFiniteIntegral, lintegral_add_measure] at *
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.718349
δ : Type ?u.718352
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hμ : (∫⁻ (a : α), ↑‖f a‖₊ ∂μ) < ⊤
hν : (∫⁻ (a : α), ↑‖f a‖₊ ∂ν) < ⊤
⊢ ((∫⁻ (a : α), ↑‖f a‖₊ ∂μ) + ∫⁻ (a : α), ↑‖f a‖₊ ∂ν) < ⊤
exact add_lt_top.2 ⟨hμ, hν⟩