instFullIncl — Mathlib

English

The inclusion functor from finite types into the ambient type category is full: every function between finite types is realized by a morphism between their carriers.

Русский

Включение конечных типов в категорию произвольных типов полно: любая функция между носителями конечных типов является морфизмом между носителями.

LaTeX

$$$\\operatorname{Hom}_{\\mathrm{FintypeCat}}(X,Y) = \\operatorname{Hom}(X.\\mathrm{carrier}, Y.\\mathrm{carrier})$$$

Lean4

instance : incl.Full :=
  InducedCategory.full _

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