α : Type u_2
E : Type u_1
F : Type ?u.934741
G : Type ?u.934744
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
⊢ 0 < ⊤
α : Type u_2
E : Type u_1
F : Type ?u.934741
G : Type ?u.934744
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
⊢ snorm 0 p μ < ⊤
rw [snorm_zero]
no goals
α : Type u_2
E : Type u_1
F : Type ?u.934741
G : Type ?u.934744
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
⊢ 0 < ⊤
exact ENNReal.coe_lt_top