instT0Space

Mathlib.Topology.CompactOpen

URI: https://scilib.ai/kg/mathlib#ContinuousMap.instT0Space

English

If Y is a T0 space, then the function space C(X,Y) is also T0.

Русский

Если Y является T0-пространством, то пространство функций C(X,Y) также T0.

LaTeX

$$$[T0Space Y] \\Rightarrow T0Space(C(X,Y))$$$

Lean4

instance [T0Space Y] : T0Space C(X, Y) :=
  t0Space_of_injective_of_continuous DFunLike.coe_injective continuous_coeFun

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

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

Разделы

Аффилиация

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