instR0SpaceProd

Mathlib.Topology.Separation.Basic

URI: https://scilib.ai/kg/mathlib#instR0SpaceProd

English

If X and Y are R0 spaces, then their product X × Y is R0.

Русский

Если X и Y — пространства R0, то их произведение X × Y также является R0.

LaTeX

$$$R0Space (X \\times Y)$$$

Lean4

instance [TopologicalSpace Y] [R0Space Y] : R0Space (X × Y) where
  specializes_symmetric _ _ h := h.fst.symm.prod h.snd.symm

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

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

Разделы

Аффилиация

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