Smoothness of projection from pi

Stream: Is there code for X?

[Oliver Nash]

I note that though we do have docs#times_cont_diff_fst, we do not seem to have:

import analysis.calculus.times_cont_diff

variables {ι 𝕜 Z : Type*}
variables [fintype ι] [nondiscrete_normed_field 𝕜] [normed_group Z] [normed_space 𝕜 Z]

lemma times_cont_diff_apply {m : with_top ℕ} (i : ι) :
  times_cont_diff 𝕜 m (λ (f : ι → Z), f i) :=
sorry

Does this follow trivially from something we do have?

[Oliver Nash]

I also note that we do have the corresponding result for continuity (in fact even in the dependent case): docs#continuous_apply

[Eric Wieser]

Do we have it with the spelling times_cont_diff 𝕜 m (function.eval i : _ → Z)?

[Oliver Nash]

I don't believe we do.

[Heather Macbeth]

@Oliver Nash It's smooth because it's linear!

lemma times_cont_diff_apply {m : with_top ℕ} (i : ι) :
  times_cont_diff 𝕜 m (λ (f : ι → Z), f i) :=
(continuous_linear_map.proj i : (ι → Z) →L[𝕜] Z).times_cont_diff

[Oliver Nash]

Ha ha, of course :face_palm:‍♂️ Thank you very much 🙂