differentiableWithinAt — Mathlib

English

If ContDiffWithinAt 𝕜 n f s x holds with n ≥ 1, then f is differentiable within s at x.

Русский

Если ContDiffWithinAt 𝕜 n f s x, тогда f дифференцируема внутри s в x.

LaTeX

$$$\text{ContDiffWithinAt}_{\mathbb{K}}(n,f;s;x) \rightarrow \text{DifferentiableWithinAt}_{\mathbb{K}}(f;s;x) \quad (1 \le n)$$$

Lean4

theorem differentiableWithinAt (h : ContDiffWithinAt 𝕜 n f s x) (hn : 1 ≤ n) : DifferentiableWithinAt 𝕜 f s x :=
  (h.differentiableWithinAt' hn).mono (subset_insert x s)

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