instR0Space

Mathlib.Topology.CompactOpen

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

English

If Y is an R0 space, then C(X,Y) is R0.

Русский

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

LaTeX

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

Lean4

instance [R0Space Y] : R0Space C(X, Y) where
  specializes_symmetric f g
    h := by
    rw [← specializes_coe] at h ⊢
    exact h.symm

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

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

Разделы

Аффилиация

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