instT2Space

Mathlib.Topology.ContinuousMap.ContinuousMapZero

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

English

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

Русский

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

LaTeX

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

Lean4

instance [T2Space R] : T2Space C(X, R)₀ :=
  isEmbedding_toContinuousMap.t2Space

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

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

Разделы

Аффилиация

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