zag_of_zag_obj

Mathlib.CategoryTheory.IsConnected

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

← MathLib Explorer

English

If F is full and Zag(F(j1), F(j2)) holds, then Zag(j1, j2) holds.

Русский

Если F полнота, и Zag(F(j1), F(j2)) верно, то Zag(j1, j2) верно.

LaTeX

$$$\forall F : J \to K\ [F.Full],\forall j_1 j_2 : J,\ Zag(F(j_1), F(j_2)) \Rightarrow Zag(j_1, j_2)$$$

Lean4

theorem zag_of_zag_obj (F : J ⥤ K) [F.Full] {j₁ j₂ : J} (h : Zag (F.obj j₁) (F.obj j₂)) : Zag j₁ j₂ :=
  Or.imp (Nonempty.map F.preimage) (Nonempty.map F.preimage) h

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

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

Разделы

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

Аффилиация

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