instT0Space — Mathlib

English

If X and Y are T0 spaces, then the product X × Y is a T0 space.

Русский

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

LaTeX

$$$\text{If } X,Y\text{ are T0 spaces, then } X\times Y\text{ is T0}.$$$

Lean4

instance instT0Space [TopologicalSpace Y] [T0Space X] [T0Space Y] : T0Space (X × Y) :=
  ⟨fun _ _ h => Prod.ext (h.map continuous_fst).eq (h.map continuous_snd).eq⟩

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