contMDiffWithinAt — Mathlib

English

For any L: E →L 𝕜 F, ContMDiffWithinAt 𝓘(𝕜,E) 𝓘(𝕜,F) n L s x holds for any set s and point x.

Русский

Для любого линейного отображения L сохраняется ContMDiffWithinAt на любой заданный множество и точку.

LaTeX

$$$\\forall L,\\ \\forall s,\\forall x:\\ ContMDiffWithinAt 𝓘(𝕜,E) 𝓘(𝕜,F) n L s x.$$$

Lean4

theorem contMDiffWithinAt (L : E →L[𝕜] F) {s x} : ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, F) n L s x :=
  L.contMDiffAt.contMDiffWithinAt

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