existsUnique — Mathlib

English

Restating the definition of a limit cone: for a limit t and any cone s, there exists a unique map l: s.pt ⟶ t.pt such that for every j, l ≫ t.π.app j = s.π.app j.

Русский

Переформулируя определение предельного конуса: для предельного конуса t и любого конуса s существует единственный морфизм l: s.pt ⟶ t.pt такой, что для каждого j выполняется l ≫ t.π.app j = s.π.app j.

LaTeX

$$$\\exists! l : s.pt \\to t.pt, \\forall j,\\; l \\gg t.π.app j = s.π.app j$$$

Lean4

/-- Restating the definition of a limit cone in terms of the ∃! operator. -/
theorem existsUnique {t : Cone F} (h : IsLimit t) (s : Cone F) : ∃! l : s.pt ⟶ t.pt, ∀ j, l ≫ t.π.app j = s.π.app j :=
  ⟨h.lift s, h.fac s, h.uniq s⟩

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