finallySmall_of_essentiallySmall — Mathlib

English

Every category J admits a FinallySmall structure from a small witness; equivalently, a constructor for FinallySmall J from a small category S with a final functor F: S ⥤ J.

Русский

Каждая категория J имеет FinallySmall структуру, получаемую из малой свидетельности; конструктор FinallySmall J из небольшой категории S с финальным функтором F: S ⥤ J.

LaTeX

$$$[\\text{FinallySmall}\\; J] = \\exists S\\;[\\text{SmallCategory } S]\\, (F : S \\to J)\\;[F\\text{ Final}]$$

Lean4

theorem finallySmall_of_essentiallySmall [EssentiallySmall.{w} J] : FinallySmall.{w} J :=
  FinallySmall.mk' (equivSmallModel.{w} J).inverse

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