α : Type u_2
β : Type u_1
γ : Type ?u.1329799
δ : Type ?u.1329802
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hf : Integrable f
⊢ (∫⁻ (a : α), ↑‖f a‖₊ ∂μ) = ∫⁻ (a : α), edist (f a) 0 ∂μ
α : Type u_2
β : Type u_1
γ : Type ?u.1329799
δ : Type ?u.1329802
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hf : Integrable f
⊢ edist (toL1 f hf) 0 = ∫⁻ (a : α), edist (f a) 0 ∂μ
simp [Integrable.toL1, snorm, snorm']
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.1329799
δ : Type ?u.1329802
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hf : Integrable f
⊢ (∫⁻ (a : α), ↑‖f a‖₊ ∂μ) = ∫⁻ (a : α), edist (f a) 0 ∂μ
simp [edist_eq_coe_nnnorm]