pith. machine review for the scientific record. sign in
lemma proved tactic proof

phi_contDiff_succ

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

 139private lemma phi_contDiff_succ (H : ℝ → ℝ) (h_cont : Continuous H) {n : ℕ}
 140    (h : ContDiff ℝ (n : ℕ∞) H) : ContDiff ℝ ((n + 1 : ℕ) : ℕ∞) (Phi H) := by

proof body

Tactic-mode proof.

 141  suffices ContDiff ℝ ((n : ℕ∞) + 1) (Phi H) by exact_mod_cast this
 142  rw [contDiff_succ_iff_deriv]
 143  exact ⟨phi_differentiable H h_cont,
 144    fun h_omega => absurd h_omega (by exact_mod_cast WithTop.coe_ne_top),
 145    by rwa [deriv_phi_eq H h_cont]⟩
 146

used by (3)

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

depends on (9)

Lean names referenced from this declaration's body.