isPreconnected_of_subsingleton

Mathlib.CategoryTheory.IsConnected

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

← MathLib Explorer

English

If J is a Subsingleton category, then J is preconnected.

Русский

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

LaTeX

$$$ [Subsingleton(J)] \\Rightarrow IsPreconnected(J)$$

Lean4

instance isPreconnected_of_subsingleton [Subsingleton J] : IsPreconnected J where
  iso_constant {α} F j := ⟨NatIso.ofComponents (fun x ↦ eqToIso (by simp [Subsingleton.allEq x j]))⟩

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

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

Разделы

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

Аффилиация

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