no goals
α : Type u_3
E : Type u_1
F : Type u_2
G : Type ?u.2832703
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
g✝ : E → F
c : ℝ≥0
inst✝ : Fact (1 ≤ p)
hg : LipschitzWith c g✝
g0 : g✝ 0 = 0
f g : { x // x ∈ Lp E p }
⊢ dist (compLp hg g0 f) (compLp hg g0 g) ≤ ↑c * dist f g
simp [dist_eq_norm, norm_compLp_sub_le]