chore(analysis/calculus/cont_diff): Add two helper lemmas (#15894)

This PR adds the forward direction of `cont_diff_iff_continuous_differentiable` as separate lemmas, which enables using dot-notation for `cont_diff`.

src/analysis/calculus/cont_diff.lean

@@ -1519,6 +1519,16 @@ by simp [cont_diff_on_univ.symm, continuous_iff_continuous_on_univ,
     differentiable_on_univ.symm, iterated_fderiv_within_univ,
     cont_diff_on_iff_continuous_on_differentiable_on unique_diff_on_univ]
 
+/-- If `f` is `C^n` then its `m`-times iterated derivative is continuous for `m ≤ n`. -/
+lemma cont_diff.continuous_iterated_fderiv {m : ℕ} (hm : (m : with_top ℕ) ≤ n)
+  (hf : cont_diff 𝕜 n f) : continuous (λ x, iterated_fderiv 𝕜 m f x) :=
+(cont_diff_iff_continuous_differentiable.mp hf).1 m hm
+
+/-- If `f` is `C^n` then its `m`-times iterated derivative is differentiable for `m < n`. -/
+lemma cont_diff.differentiable_iterated_fderiv {m : ℕ} (hm : (m : with_top ℕ) < n)
+  (hf : cont_diff 𝕜 n f) : differentiable 𝕜 (λ x, iterated_fderiv 𝕜 m f x) :=
+(cont_diff_iff_continuous_differentiable.mp hf).2 m hm
+
 lemma cont_diff_of_differentiable_iterated_fderiv
   (h : ∀(m : ℕ), (m : with_top ℕ) ≤ n → differentiable 𝕜 (iterated_fderiv 𝕜 m f)) :
   cont_diff 𝕜 n f :=