α : Type u_3
E : Type u_1
F : Type u_2
G : Type ?u.2123310
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
⊢ ↑↑(compLp hg g0 0) =ᵐ[μ] 0
α : Type u_3
E : Type u_1
F : Type u_2
G : Type ?u.2123310
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
⊢ compLp hg g0 0 = 0
rw [Lp.eq_zero_iff_ae_eq_zero]
α : Type u_3
E : Type u_1
F : Type u_2
G : Type ?u.2123310
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
⊢ g ∘ ↑↑0 =ᵐ[μ] 0
α : Type u_3
E : Type u_1
F : Type u_2
G : Type ?u.2123310
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
⊢ ↑↑(compLp hg g0 0) =ᵐ[μ] 0
apply (coeFn_compLp _ _ _).trans
case h
α : Type u_3
E : Type u_1
F : Type u_2
G : Type ?u.2123310
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
a✝ : α
ha : ↑↑0 a✝ = OfNat.ofNat 0 a✝
⊢ (g ∘ ↑↑0) a✝ = OfNat.ofNat 0 a✝
α : Type u_3
E : Type u_1
F : Type u_2
G : Type ?u.2123310
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
⊢ g ∘ ↑↑0 =ᵐ[μ] 0
filter_upwards [Lp.coeFn_zero E p μ] with _ ha
no goals
case h
α : Type u_3
E : Type u_1
F : Type u_2
G : Type ?u.2123310
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
a✝ : α
ha : ↑↑0 a✝ = OfNat.ofNat 0 a✝
⊢ (g ∘ ↑↑0) a✝ = OfNat.ofNat 0 a✝
simp only [ha, g0, Function.comp_apply, Pi.zero_apply]