instEssentiallySmallOpposite — Mathlib

English

If there exists an equivalence between C and a small category S, then C is essentially small.

Русский

Если существует эквивалентность между C и малой категорией S, то C по существу мала.

LaTeX

$$$\exists S [SmallCategory S], (\!C\! ) \simeq S \Rightarrow \operatorname{EssentiallySmall}(C)$$$

Lean4

instance (C : Type u) [Category.{v} C] [EssentiallySmall.{w} C] : EssentiallySmall.{w} Cᵒᵖ :=
  EssentiallySmall.mk' (equivSmallModel C).op

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