instR1Space

Mathlib.Topology.CompactOpen

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

English

If Y is a R1 space, then C(X,Y) is R1.

Русский

Если Y — R1 пространство, то C(X,Y) — R1.

LaTeX

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

Lean4

instance [R1Space Y] : R1Space C(X, Y) :=
  .of_continuous_specializes_imp continuous_coeFun fun _ _ ↦ specializes_coe.1

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

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

Разделы

Аффилиация

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