instT1SpaceProd — Mathlib

English

If X and Y are T1-spaces, then their product X × Y is a T1-space.

Русский

Если пространства X и Y являются T1-пространствами, то их произведение X × Y также является T1-пространством.

LaTeX

$$$ \forall X,Y, [TopologicalSpace X] [TopologicalSpace Y] [T1Space X] [T1Space Y] \\Rightarrow T1Space (X \times Y)$.$$

Lean4

instance [TopologicalSpace Y] [T1Space X] [T1Space Y] : T1Space (X × Y) :=
  ⟨fun ⟨a, b⟩ => @singleton_prod_singleton _ _ a b ▸ isClosed_singleton.prod isClosed_singleton⟩

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