English
For any diagram F: J ⥤ C with a limit D and preserved forgetful structure, two elements x,y in the underlying type if their projections are equal for all indices j, then x=y.
Русский
Для диаграммы F: J ⥤ C с пределом D и сохранением структуры забывания, если две вершины x,y в базовом типе имеют равные проекции на все индексы j, то x=y.
LaTeX
$$$\\forall F:\\, J\\to C,\\; [HasLimit\ F] \\Rightarrow \\forall x,y:\\, ToType(D.pt),\\; (\\forall j:\\, J,\\; D.\\pi_{F,j}(x)=D.\\pi_{F,j}(y))\\Rightarrow x=y$$$
Lean4
/-- If a functor `G : J ⥤ C` to a concrete category has a limit and that `forget C`
is corepresentable, then `(G ⋙ forget C).sections` is small. -/
theorem small_sections_of_hasLimit {C : Type u} [Category.{v} C] [HasForget.{v} C] [(forget C).IsCorepresentable]
{J : Type w} [Category.{t} J] (G : J ⥤ C) [HasLimit G] : Small.{v} (G ⋙ forget C).sections :=
by
rw [← Types.hasLimit_iff_small_sections]
infer_instance
