Theorem: CS.hasDerivAt (PrimeNumberTheoremAnd/Sobolev.lean)

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x✝ v : ℝ
f : CS (n + 1) E
x : ℝ
⊢ 1 ≤ ↑(n + 1)
Tactic:
simp
State after:
no goals