differentiableOn — Mathlib

English

For an affine map f: V →ᴬ[𝕜] W, the map is differentiable on any subset s ⊆ V.

Русский

Для аффинного отображения f: V →ᴬ[𝕜] W отображение дифференцируемо на любом подмножестве s ⊆ V.

LaTeX

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

Lean4

theorem differentiableOn (f : V →ᴬ[𝕜] W) {s : Set V} : DifferentiableOn 𝕜 f s :=
  f.differentiable.differentiableOn

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