bundling of a clm construction

Stream: general

[Moritz Doll]

I have the following lemma and I am not sure whether the continuity statement for the whole space should be bundled as a continuous linear map or not. I don't really see the advantage of bundling, because the _apply lemma has to carry around the assumption, so in every concrete case one wants to have separate _apply lemmas leading to a quite a bit of boilerplate.

lemma continuous_at_zero_of_locally_bounded {f : E →ₛₗ[σ] F}
  (hf : ∀ (s : set E) (hs : is_vonN_bounded 𝕜 s), is_vonN_bounded 𝕜' (f '' s)) :
  continuous_at f 0 := sorry