instR1Space

Mathlib.Topology.ContinuousMap.ContinuousMapZero

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

English

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

Русский

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

LaTeX

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

Lean4

instance [R1Space R] : R1Space C(X, R)₀ :=
  isEmbedding_toContinuousMap.r1Space

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

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

Разделы

Аффилиация

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