contMDiff — Mathlib

English

Let L be a continuous linear map between normed spaces E and F. Then L is ContMDiff of order n between the model spaces, i.e., ContMDiff 𝓘(𝕜,E) 𝓘(𝕜,F) n L.

Русский

Пусть L - непрерывное линейное отображение между нормированными пространствами E и F. Тогда L гладко порядка n между моделями пространства.

LaTeX

$$$\\displaystyle L: E \\to_L[𝕜] F \\quad\\Longrightarrow\\quad \\mathrm{ContMDiff}_{\\mathcal{I}(𝕜,E),\\mathcal{I}(𝕜,F)}^{n}(L).$$$

Lean4

theorem contMDiff (L : E →L[𝕜] F) : ContMDiff 𝓘(𝕜, E) 𝓘(𝕜, F) n L :=
  L.contDiff.contMDiff

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