instR0Space

Mathlib.Topology.ContinuousMap.ContinuousMapZero

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

English

If R is R0Space, then C(X,R)₀ is R0Space.

Русский

Если R является R0Space, то C(X,R)₀ является R0Space.

LaTeX

$$[R0Space R] ⇒ R0Space C(X,R)₀$$

Lean4

instance [R0Space R] : R0Space C(X, R)₀ :=
  isEmbedding_toContinuousMap.r0Space

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

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

Разделы

Аффилиация

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