finallySmall

Mathlib.CategoryTheory.Limits.Indization.IndObject

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.IsIndObject.finallySmall

English

From an Ind-object A, the CostructuredArrow yoneda A is finally small.

Русский

Из Ind-объекта A следует, что CostructuredArrow yoneda A является finally small.

LaTeX

$$$\mathrm{IsIndObject}(A)\Rightarrow \mathrm{FinallySmall}(\mathrm{CostructuredArrow}(\mathrm{yoneda},A))$$$

Lean4

theorem finallySmall (h : IsIndObject A) : FinallySmall.{v} (CostructuredArrow yoneda A) :=
  FinallySmall.mk' h.presentation.toCostructuredArrow

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru