instIsConnectedWidePullbackShape — Mathlib

English

The shape of a wide pullback is connected in the sense that all its arrows induce compatible morphisms that connect all objects.

Русский

Форма широкого предела связана: все стрелки индуцируют совместимые морфизмы, соединяющие все объекты.

LaTeX

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

Lean4

instance {J} : IsConnected (WidePullbackShape 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 (.term _)]

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