lemma proved term proof

`hasDerivAt_deriv_of_contDiffTwo`

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

formal statement (Lean)

  38private lemma hasDerivAt_deriv_of_contDiffTwo {Hf : ℝ → ℝ}
  39    (h_diff : ContDiff ℝ 2 Hf) (x : ℝ) :
  40    HasDerivAt (deriv Hf) (deriv (deriv Hf) x) x := by

proof body

Term-mode proof.

  41  exact (contDiffTwo_differentiable_deriv h_diff).differentiableAt.hasDerivAt
  42
  43/-- Differentiate the d'Alembert equation once in the second variable. -/

used by (1)

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

dAlembert_second_deriv_at_zero_of_contDiff in IndisputableMonolith.Cost.ContDiffReduction decl_use

depends on (1)

Lean names referenced from this declaration's body.

contDiffTwo_differentiable_deriv in IndisputableMonolith.Cost.ContDiffReduction decl_use