mk' — Mathlib

English

If J is a category with a FinallySmall structure, then the functor fromFinalModel J is final.

Русский

Если J имеет структуру FinallySmall, то fунктор fromFinalModel J финален.

LaTeX

$$$[\\text{FinallySmall}\\; J] \\Rightarrow \\text{Final}(\\mathrm{fromFinalModel}\\, J)$$$

Lean4

/-- Constructor for `FinallySmall C` from an explicit small category witness. -/
theorem mk' {J : Type u} [Category.{v} J] {S : Type w} [SmallCategory S] (F : S ⥤ J) [Final F] : FinallySmall.{w} J :=
  ⟨S, _, F, inferInstance⟩

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