instRegularSpace

Mathlib.Topology.ContinuousMap.ContinuousMapZero

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

English

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

Русский

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

LaTeX

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

Lean4

instance [RegularSpace R] : RegularSpace C(X, R)₀ :=
  isEmbedding_toContinuousMap.regularSpace

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

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

Разделы

Аффилиация

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