differentiableWithinAt — Mathlib

English

For a continuous affine map f: V →ᴬ[𝕜] W and any set s and point x, DifferentiableWithinAt 𝕜 f s x holds.

Русский

Для непрерывного афинного отображения f: V →ᴬ[𝕜] W и любого множества s и точки x выполняется DifferentiableWithinAt 𝕜 f s x.

LaTeX

$$$ \operatorname{DifferentiableWithinAt}_{\mathbb{k}}(f, s, x). $$$

Lean4

theorem differentiableWithinAt (f : V →ᴬ[𝕜] W) {s : Set V} {x : V} : DifferentiableWithinAt 𝕜 f s x :=
  f.differentiableAt.differentiableWithinAt

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