isConnected_of_nonempty_and_subsingleton

Mathlib.CategoryTheory.IsConnected

URI: https://scilib.ai/kg/mathlib#CategoryTheory.isConnected_of_nonempty_and_subsingleton

English

If J is nonempty and Subsingleton, then J is connected.

Русский

Если J ненулева и подселединта, тогда J связна.

LaTeX

$$$ [Nonempty(J)] \\land [Subsingleton(J)] \\Rightarrow IsConnected(J)$$

Lean4

instance isConnected_of_nonempty_and_subsingleton [Nonempty J] [Subsingleton J] : IsConnected J where

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

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

Разделы

Аффилиация

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