C² implies C¹

Stream: new members

[Michael Rothgang]

Seems obvious, but I couldn't find this in mathlib. Minimized code:

lemma diff {E F : Type*} {r : ℕ} (hr : r ≥ 1) {w : Set E}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F]
  {f : E → F} (hf : ContDiffOn ℝ (↑r) f w) : ContDiffOn ℝ 1 f w := sorry

[Kyle Miller]

Is this docs#ContDiffOn.of_le applied to hr? (Maybe you need to transform hr)

[Michael Rothgang]

Looks promising, let me check...

[Kyle Miller]

The proof of docs#ContDiffOn.one_of_succ looks helpful to see how to transform hr

[Michael Rothgang]

Works like a charm, thanks! (I need to transform hr.)