instIsConnectedWidePushoutShape

Mathlib.CategoryTheory.Limits.Shapes.Connected

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

← MathLib Explorer

English

Similarly, the wide pushout shape is connected.

Русский

Аналогично, форма широкого пушапа связана.

LaTeX

$$$\\text{IsConnected}(\\mathrm{WidePushoutShape}\\ J)$$$

Lean4

instance {J} : IsConnected (WidePushoutShape J) :=
  by
  apply IsConnected.of_constant_of_preserves_morphisms
  intro α F H
  suffices ∀ i, F i = F none from fun j j' ↦ (this j).trans (this j').symm
  rintro ⟨⟩
  exacts [rfl, (H (.init _)).symm]

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

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

Разделы

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

Аффилиация

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