continuous_restrictScalars

Mathlib.Topology.Algebra.Module.Multilinear.Topology

URI: https://scilib.ai/kg/mathlib#ContinuousMultilinearMap.continuous_restrictScalars

← MathLib Explorer

English

If F is T2, then CM_k(E,F) is T2 as an instance.

Русский

Если F T2, то CM_k(E,F) является T2 в виде инстанса.

LaTeX

$$$[T2Space F] \\Rightarrow T2Space (\\mathrm{CM}_k(E,F))$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru