English
The topology on the product X × Y is the initial (product) topology, i.e., the coarsest topology making the projections onto X and Y continuous.
Русский
Топология на произведении X × Y — начальная (произведение) топология, наименьшая по силе, делающая проекции на X и Y непрерывными.
LaTeX
$$$\\text{Top}(X\\times Y) = \\text{induced}(\\text{Prod.fst}, t_X) \\cap \\text{induced}(\\text{Prod.snd}, t_Y).$$$
Lean4
instance instTopologicalSpaceProd [t₁ : TopologicalSpace X] [t₂ : TopologicalSpace Y] : TopologicalSpace (X × Y) :=
induced Prod.fst t₁ ⊓ induced Prod.snd t₂