instTopologicalSpaceModelPi

Mathlib.Geometry.Manifold.ChartedSpace

URI: https://scilib.ai/kg/mathlib#instTopologicalSpaceModelPi

English

The product of indexed spaces carries the product topology given by Pi.topologicalSpace.

Русский

Произведение индексированных пространств носит произведённую топологию, заданную Pi.topologicalSpace.

LaTeX

$$instTopologicalSpaceModelPi$$

Lean4

instance [∀ i, TopologicalSpace (Hi i)] : TopologicalSpace (ModelPi Hi) :=
  Pi.topologicalSpace

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru