finallySmall_of_final_of_finallySmall

English

If J is FinallySmall, there exists a small set of objects s and, for every i in J, a nonempty hom-set i ⟶ j for some j in s.

Русский

Если J является FinallySmall, существует малый набор объектов s и для каждого i в J непустое множество гомоморфизмов i ⟶ j для некоторого j в s.

LaTeX

$$$\\exists s\\subset J,\\; \\#s<\\infty,\\; \\forall i,\\ \\exists j\\in s,\\; \\operatorname{Nonempty}(i \\to j)$$$

Lean4

theorem finallySmall_of_final_of_finallySmall [FinallySmall.{w} K] (F : K ⥤ J) [Final F] : FinallySmall.{w} J :=
  suffices Final ((fromFinalModel K) ⋙ F) from .mk' ((fromFinalModel K) ⋙ F)
  final_comp _ _

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