eventually_differentiableAt — Mathlib

English

If f is differentiable on a set near x, then there exists a neighborhood of x on which f is differentiable at every point.

Русский

Если f дифференцируема на окрестности x, то существует окрестность x, на которой f дифференцируема в каждой точке.

LaTeX

$$$DifferentiableOn\ 𝕜\ f\ s \land s\in 𝓝 x\Rightarrow\forall y\in s, DifferentiableAt\ 𝕜\ f\ y$$$

Lean4

theorem eventually_differentiableAt (h : DifferentiableOn 𝕜 f s) (hs : s ∈ 𝓝 x) : ∀ᶠ y in 𝓝 x, DifferentiableAt 𝕜 f y :=
  (eventually_eventually_nhds.2 hs).mono fun _ => h.differentiableAt

Похожие утверждения