Zulip Chat Archive

Stream: general

Topic: bundling of a clm construction

Moritz Doll (Sep 21 2022 at 17:32):

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

Last updated: Dec 20 2023 at 11:08 UTC