existsUnique — Mathlib

English

For any cone t over F with HasLimit F, there exists a unique l: t.pt ⟶ limit F such that l ≫ limit.π F j = t.π.app j for all j.

Русский

Для любого конуса t над F с HasLimit F существует единственный л: t.pt ⟶ limit F такой, что l ≫ limit.π F j = t.π.app j для всех j.

LaTeX

$$$\\exists!\\, l : t.pt \\to \\mathrm{limit} F, \\; \\forall j, \\; l \\;\\gg\\; \\mathrm{limit}.\\pi F j = t.\\pi.app j$$$

Lean4

theorem existsUnique {F : J ⥤ C} [HasLimit F] (t : Cone F) : ∃! l : t.pt ⟶ limit F, ∀ j, l ≫ limit.π F j = t.π.app j :=
  (limit.isLimit F).existsUnique _

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