instTopologicalSpaceProd — Mathlib

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₂

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