final_fromFinalModel

Mathlib.CategoryTheory.Limits.FinallySmall

URI: https://scilib.ai/kg/mathlib#CategoryTheory.final_fromFinalModel

← MathLib Explorer

English

As above: fromFinalModel J is final when J is FinallySmall.

Русский

Как и выше: fromFinalModel J финален при FinallySmall J.

LaTeX

$$$\\text{Final}(\\mathrm{fromFinalModel}\\, J)$$$

Lean4

instance final_fromFinalModel [FinallySmall.{w} J] : Final (fromFinalModel J) :=
  Classical.choose_spec (Classical.choose_spec (Classical.choose_spec (@FinallySmall.final_smallCategory J _ _)))

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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