isConnected_op

Mathlib.CategoryTheory.IsConnected

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

← MathLib Explorer

English

If J is connected, then Jᵒᵖ is connected.

Русский

Если J связно, то Jᵒᵖ связно.

LaTeX

$$$[\\operatorname{IsConnected}(J)] \\Rightarrow \\operatorname{IsConnected}(J^{\\mathrm{op}})$$$

Lean4

/-- If `J` is connected, then `Jᵒᵖ` is connected as well. -/
instance isConnected_op [IsConnected J] : IsConnected Jᵒᵖ where
  is_nonempty := Nonempty.intro (op (Classical.arbitrary J))

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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