Theorem: SchwartzMap.snorm_nnreal_lt_top (ForML/SchwartzLp.lean)

State before:
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
mE : MeasureSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
f : 𝓢(E, F)
p : NNReal
hp : 0 < p
⊢ snorm (⇑f) (↑p) volume < ⊤
Tactic:
simpa using snorm_nnreal_one_add_norm_rpow_smul_lt_top 0 f hp
State after:
no goals