no goals
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
inst✝ : MeasurableSpace α
p : ℝ≥0∞
f : ι → α → β
ε : ℝ
x✝² : 0 < ε
i : ι
s : Set α
x✝¹ : MeasurableSet s
x✝ : ↑↑0 s ≤ ENNReal.ofReal 1
⊢ snorm (Set.indicator s (f i)) p 0 ≤ ENNReal.ofReal ε
simp