topologicalSpace — Mathlib

English

PiLp p β carries the product topology, i.e., the topology is the product of the coordinate spaces.

Русский

PiLp p β оснащено произведенной топологией; топология есть произведение топологий координат.

LaTeX

$$$$\\text{TopologicalSpace}(\\PiLp(p,\\beta))=\\text{prod topology over }\\{\\beta_i\\}.$$$

Lean4

instance topologicalSpace [∀ i, TopologicalSpace (β i)] : TopologicalSpace (PiLp p β) :=
  inferInstanceAs <| TopologicalSpace (Π i, β i)

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