English
If ContDiffWithinAt 𝕜 n f s x holds with n ≥ 1, then f is differentiable within s at x.
Русский
Если функция C^n внутри множества s в точке x, то она дифференцируема внутри s в x, при n ≥ 1.
LaTeX
$$$\text{ContDiffWithinAt}_{\mathbb{K}}(n,f;s;x) \land 1 \le n \quad\Rightarrow\quad \text{DifferentiableWithinAt}_{\mathbb{K}}(f;s;x)$$$
Lean4
/-- If a function is `C^n` within a set at a point, with `n ≥ 1`, then it is differentiable
within this set at this point. -/
theorem differentiableWithinAt' (h : ContDiffWithinAt 𝕜 n f s x) (hn : 1 ≤ n) :
DifferentiableWithinAt 𝕜 f (insert x s) x :=
by
rcases contDiffWithinAt_nat.1 (h.of_le hn) with ⟨u, hu, p, H⟩
rcases mem_nhdsWithin.1 hu with ⟨t, t_open, xt, tu⟩
rw [inter_comm] at tu
exact
(differentiableWithinAt_inter (IsOpen.mem_nhds t_open xt)).1 <|
((H.mono tu).differentiableOn le_rfl) x ⟨mem_insert x s, xt⟩
