uniformContinuous_restrictScalars

English

Equality of linear maps: the canonical lift restrictScalarsL coincides with the standard restriction map on scalars.

Русский

Канонический переход между линейными отображениями совпадает с обычным ограничением скаляров.

LaTeX

$$$ (\\mathrm{restrictScalarsL}\\, 𝕜 E F 𝕜' 𝕜'') = \\mathrm{restrictScalars}_{𝕜'}$$$

Lean4

theorem uniformContinuous_restrictScalars : UniformContinuous (restrictScalars 𝕜' : (E →L[𝕜] F) → (E →L[𝕜'] F)) :=
  (isUniformEmbedding_restrictScalars 𝕜').uniformContinuous

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