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)

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

proof body

Tactic-mode proof.

 199  suffices ContDiff ℝ ((n : ℕ∞) + 1) (Phi H) by exact_mod_cast this
 200  rw [contDiff_succ_iff_deriv]
 201  exact ⟨phi_differentiable H h_cont,
 202    fun h_omega => absurd h_omega (by exact_mod_cast WithTop.coe_ne_top),
 203    by rwa [deriv_phi_eq H h_cont]⟩
 204
 205/-- Core bootstrap: continuous d'Alembert → C^n for all n. -/

used by (3)

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

depends on (14)

Lean names referenced from this declaration's body.