initiallySmall_of_initial_of_essentiallySmall

English

If K is EssentiallySmall and F : K ⥤ J is Initial, then J is InitiallySmall.

Русский

Если K является EssentiallySmall и F : K ⥤ J начальная, то J – InitiallySmall.

LaTeX

$$$[\\text{EssentiallySmall } K] \\land [\\text{Initial } F] \\Rightarrow [\\text{InitiallySmall } J]$$$

Lean4

theorem initiallySmall_of_initial_of_essentiallySmall [EssentiallySmall.{w} K] (F : K ⥤ J) [Initial F] :
    InitiallySmall.{w} J :=
  have := initiallySmall_of_essentiallySmall K
  initiallySmall_of_initial_of_initiallySmall F

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