continuous_restrictScalars — Mathlib

English

The map restricting scalars is continuous, i.e., small changes in input lead to small changes in the restricted output space.

Русский

Отображение ограничения скаляров непрерывно: малые изменения входа приводят к малым изменениям на выходе после ограничения.

LaTeX

$$$\\text{continuous}(\\operatorname{restrictScalars}_{\\mathbb{k}'})$$$

Lean4

@[continuity, fun_prop]
theorem continuous_restrictScalars : Continuous (restrictScalars 𝕜' : E [⋀^ι]→L[𝕜] F → E [⋀^ι]→L[𝕜'] F) :=
  isEmbedding_restrictScalars.continuous

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