limit_ext — Mathlib

English

Equivalence between equality of colimit injections and the existence of a joint epimorphic representation through some common object.

Русский

Эквивалентность между равенством инъекций колимита и существованием совместного представления через общее объект.

LaTeX

$$$\\forall i,j:\\, J,\\; x:\\, F.obj i,\\; y:\\, F.obj j,\\; (\\mathrm{colimit}.\\iota F i x = \\mathrm{colimit}.\\iota F j y) \\iff \\exists k,f,g:\\, i\\to k, j\\to k, F.map f x = F.map g y$$$

Lean4

theorem limit_ext [HasLimit F] (x y : ToType (limit F)) : (∀ j, limit.π F j x = limit.π F j y) → x = y :=
  Concrete.isLimit_ext F (limit.isLimit _) _ _

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