isConnected_of_isInitial — Mathlib

English

If there exists an initial object in a category, then the category is connected.

Русский

Если в категории существует начальный объект, то категория связна.

LaTeX

$$$\text{IsConnected}(C)$$$

Lean4

/-- Prove that a category is connected by supplying an explicit initial object. -/
theorem isConnected_of_isInitial {x : C} (h : Limits.IsInitial x) : IsConnected C :=
  by
  letI : Nonempty C := ⟨x⟩
  apply isConnected_of_zigzag
  intro j₁ j₂
  use [x, j₂]
  simp only [List.isChain_cons_cons, List.isChain_singleton, and_true, ne_eq, reduceCtorEq, not_false_eq_true,
    List.getLast_cons, List.cons_ne_self, List.getLast_singleton]
  exact ⟨Zag.symm <| Zag.of_hom <| h.to _, Zag.of_hom <| h.to _⟩

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