instConnectedSpaceProd

Mathlib.Topology.Connected.Basic

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

English

If each X_i is a connected space, then the product ∏_i X_i is connected.

Русский

Если для каждого i пространство X_i связано, то произведение ∏_i X_i связано.

LaTeX

$$$$\\text{ConnectedSpace}(\\prod_{i} X_i)$$$$

Lean4

instance [TopologicalSpace β] [ConnectedSpace α] [ConnectedSpace β] : ConnectedSpace (α × β) :=
  ⟨inferInstance⟩

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

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

Разделы

Аффилиация

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