lemma proved wrapper

`contDiffTwo_differentiable`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  27private lemma contDiffTwo_differentiable {Hf : ℝ → ℝ}
  28    (h_diff : ContDiff ℝ 2 Hf) : Differentiable ℝ Hf := by

One-line wrapper that applies exact.

  29  exact h_diff.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
  30

From the project-wide theorem graph. These declarations reference this one in their body.

dAlembert_cosh_solution_of_contDiff in IndisputableMonolith.Cost.ContDiffReduction decl_use
dAlembert_first_deriv_of_contDiff in IndisputableMonolith.Cost.ContDiffReduction decl_use