α : Type u_1
β : Type u_2
γ : Type ?u.1284348
δ : Type ?u.1284351
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : { x // x ∈ Lp β 1 }
⊢ (∫⁻ (a : α), ↑‖↑↑f a - ↑↑g a‖₊ ∂μ) = ∫⁻ (a : α), edist (↑↑f a) (↑↑g a) ∂μ
α : Type u_1
β : Type u_2
γ : Type ?u.1284348
δ : Type ?u.1284351
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : { x // x ∈ Lp β 1 }
⊢ edist f g = ∫⁻ (a : α), edist (↑↑f a) (↑↑g a) ∂μ
simp [Lp.edist_def, snorm, snorm']
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.1284348
δ : Type ?u.1284351
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : { x // x ∈ Lp β 1 }
⊢ (∫⁻ (a : α), ↑‖↑↑f a - ↑↑g a‖₊ ∂μ) = ∫⁻ (a : α), edist (↑↑f a) (↑↑g a) ∂μ
simp [edist_eq_coe_nnnorm_sub]