instT3Space

Mathlib.Topology.ContinuousMap.ContinuousMapZero

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

English

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

Русский

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

LaTeX

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

Lean4

instance [T3Space R] : T3Space C(X, R)₀ :=
  isEmbedding_toContinuousMap.t3Space

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

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

Разделы

Аффилиация

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