isConnected_of_isTerminal — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- Prove that a category is connected by supplying an explicit terminal object. -/
theorem isConnected_of_isTerminal {x : C} (h : Limits.IsTerminal 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.of_hom <| h.from _, Zag.symm <| Zag.of_hom <| h.from _⟩
      -- note : it seems making the following two as instances breaks things, so these are lemmas.

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