modelPiInhabited

Mathlib.Geometry.Manifold.ChartedSpace

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

English

The model product of topological spaces carries the product topology

Русский

Модельное произведение топологических пространств обладает произведённой топологией

LaTeX

$$instTopologicalSpaceModelPi$$

Lean4

instance modelPiInhabited [∀ i, Inhabited (Hi i)] : Inhabited (ModelPi Hi) :=
  Pi.instInhabited

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

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

Разделы

Аффилиация

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