toTopologicalSpace_prod — Mathlib

English

The topological space associated to the product of uniform spaces coincides with the product topology.

Русский

Обобщение пространства сверху произведения равномерных пространств совпадает с произведением топологий.

LaTeX

$$$\operatorname{toTopologicalSpace}(\text{instUniformSpaceProd}) = \operatorname{instTopologicalSpaceProd}$$$

Lean4

theorem toTopologicalSpace_prod {α} {β} [u : UniformSpace α] [v : UniformSpace β] :
    @UniformSpace.toTopologicalSpace (α × β) instUniformSpaceProd =
      @instTopologicalSpaceProd α β u.toTopologicalSpace v.toTopologicalSpace :=
  rfl

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