existsUnique — Mathlib

English

Given a colimit cocone t and any cocone s, there exists a unique morphism d: t.pt ⟶ s.pt such that for every j in J, t.ι.app j ≫ d = s.ι.app j.

Русский

Пусть t — колимитный кокон, и пусть s — любой кокон. Существует единственный морфизм d: t.pt → s.pt, такой что для каждого j ∈ J выполняется t.ι.app j ≫ d = s.ι.app j.

LaTeX

$$$ \exists! d : t.pt ⟶ s.pt, \; \forall j,\ t.ι.app j \;≫\; d = s.ι.app j $$$

Lean4

/-- Restating the definition of a colimit cocone in terms of the ∃! operator. -/
theorem existsUnique {t : Cocone F} (h : IsColimit t) (s : Cocone F) :
    ∃! d : t.pt ⟶ s.pt, ∀ j, t.ι.app j ≫ d = s.ι.app j :=
  ⟨h.desc s, h.fac s, h.uniq s⟩

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