instT2Space

Mathlib.Topology.Algebra.Module.Multilinear.Topology

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

English

If F is a T2 space, CM_k(E,F) is T3 (regular).

Русский

Если F — пространство T2, CM_k(E,F) является T3 (регулярное).

LaTeX

$$$\\text{If } F \\text{ is } T_2,\\, \\mathrm{CM}_k(E,F) \\text{ is } T_3$.$$

Lean4

instance instT2Space [T2Space F] : T2Space (ContinuousMultilinearMap 𝕜 E F) :=
  .of_injective_continuous DFunLike.coe_injective continuous_coeFun

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

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

Разделы

Аффилиация

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