α : Type u_2
β : Type u_1
γ : Type ?u.936048
δ : Type ?u.936051
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : α → β
hf : Integrable f
hg : Integrable g
⊢ (HasFiniteIntegral fun a => f a) ∧ HasFiniteIntegral fun a => g a
α : Type u_2
β : Type u_1
γ : Type ?u.936048
δ : Type ?u.936051
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : α → β
hf : Integrable f
hg : Integrable g
⊢ (∫⁻ (a : α), edist (f a) (OfNat.ofNat 0 a) ∂μ) < ⊤ ∧ (∫⁻ (a : α), edist (g a) (OfNat.ofNat 0 a) ∂μ) < ⊤
simp_rw [Pi.zero_apply, ← hasFiniteIntegral_iff_edist]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.936048
δ : Type ?u.936051
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : α → β
hf : Integrable f
hg : Integrable g
⊢ (HasFiniteIntegral fun a => f a) ∧ HasFiniteIntegral fun a => g a
exact ⟨hf.hasFiniteIntegral, hg.hasFiniteIntegral⟩