lemma proved term proof

`contDiffTwo_differentiable_deriv`

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

formal statement (Lean)

  31private lemma contDiffTwo_differentiable_deriv {Hf : ℝ → ℝ}
  32    (h_diff : ContDiff ℝ 2 Hf) : Differentiable ℝ (deriv Hf) := by

proof body

Term-mode proof.

  33  have h_diff' := h_diff
  34  rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h_diff'
  35  rw [contDiff_succ_iff_deriv] at h_diff'
  36  exact h_diff'.2.2.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
  37

used by (1)

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

hasDerivAt_deriv_of_contDiffTwo in IndisputableMonolith.Cost.ContDiffReduction decl_use

depends on (1)

Lean names referenced from this declaration's body.

from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use