instSmallHom — Mathlib

English

For any category C and X,Y in LightCondensed C, the hom-set Hom_{LightCondensed(C)}(X,Y) is a small type.

Русский

Для любой категории C и X,Y ∈ LightCondensed(C) множество морфизмов Hom_{LightCondensed(C)}(X,Y) является малым типом.

LaTeX

$$$\operatorname{Small}\bigl(\mathrm{Hom}_{\mathrm{LightCondensed}(C)}(X,Y)\bigr)$$$

Lean4

instance (X Y : LightCondensed.{u} C) : Small.{max u v} (X ⟶ Y) where
  equiv_small :=
    ⟨(equivSmall C).functor.obj X ⟶ (equivSmall C).functor.obj Y, ⟨(equivSmall C).fullyFaithfulFunctor.homEquiv⟩⟩

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