mk' — Mathlib

English

There is a constructor for InitiallySmall from an explicit small witness F: S ⥤ J with F Initial.

Русский

Существует конструктор InitiallySmall, получаемый из явного малого доказательства F: S ⥤ J с F Initial.

LaTeX

$$$[\\text{SmallCategory } S]\\; (F:S\\to J)\\;[F\\ Initial] \\Rightarrow \\text{InitiallySmall } J$$$

Lean4

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

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