prod

Mathlib.CategoryTheory.IsConnected

URI: https://scilib.ai/kg/mathlib#CategoryTheory.IsConnected.prod

English

If J and K are connected, then J × K is connected.

Русский

Если J и K связаны, то их произведение связано.

LaTeX

$$$[IsConnected(J)] [IsConnected(K)] \\Rightarrow IsConnected(J \\times K)$$$

Lean4

instance prod [IsConnected J] [IsConnected K] : IsConnected (J × K) where

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

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

Разделы

Аффилиация

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