instIsConnected — Mathlib

English

A sifted category is connected; any two objects can be connected by a zigzag.

Русский

Ситообразная категория связна; любые два объекта можно соединить зигзагообразной цепью.

LaTeX

$$IsConnected C$$

Lean4

/-- A sifted category is connected. -/
instance [IsSifted C] : IsConnected C :=
  isConnected_of_zigzag
    (by
      intro c₁ c₂
      have X : StructuredArrow (c₁, c₂) (diag C) :=
        letI S : Final (diag C) := by infer_instance
        Nonempty.some (S.out (c₁, c₂)).is_nonempty
      use [X.right, c₂]
      constructor
      · constructor
        · exact Zag.of_hom X.hom.fst
        · simpa using Zag.of_inv X.hom.snd
      · rfl)

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