instT2Space

Mathlib.Topology.Instances.TrivSqZeroExt

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

English

If R and M are T2 spaces, then tsze R M is a T2 space.

Русский

Если R и M — пространство T2, то tsze R M также является пространством T2.

LaTeX

$$$\\text{If } T2Space(R) \\text{ and } T2Space(M),\\; T2Space(tsze\\,R\\,M).$$$

Lean4

instance [T2Space R] [T2Space M] : T2Space (tsze R M) :=
  Prod.t2Space

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

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

Разделы

Аффилиация

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