contMDiffAt — Mathlib

English

For any linear map L: E → L 𝕜 F, ContMDiffAt holds for all x, and hence ContMDiffWithinAt on any set s at any x.

Русский

Для любого линейного отображения L: E → L 𝕜 F выполняется ContMDiffAt на любой точке x, и следовательно ContMDiffWithinAt на любом множестве s в любой точке x.

LaTeX

$$$\\forall L\\; (\\mathrm{ContMDiffAt}\\; 𝓘(𝕜,E)\\; 𝓘(𝕜,F)\\; n\\; L\\; {x})$, и, следовательно, $\\mathrm{ContMDiffWithinAt}_{𝓘(𝕜,E) 𝓘(𝕜,F)}^{n}(L) s x$ для произвольных s, x.$$

Lean4

theorem contMDiffAt (L : E →L[𝕜] F) {x} : ContMDiffAt 𝓘(𝕜, E) 𝓘(𝕜, F) n L x :=
  L.contMDiff _

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