essentiallySmall_of_small_of_locallySmall

English

If C is small and locally small, then C is essentially small.

Русский

Если C малая категория и локально-малый, то C является существенно малой.

LaTeX

$$$( \text{Small}(C) \wedge \text{LocallySmall}(C) ) \Rightarrow \text{EssentiallySmall}(C)$$$

Lean4

theorem essentiallySmall_of_small_of_locallySmall [Small.{w} C] [LocallySmall.{w} C] : EssentiallySmall.{w} C :=
  (essentiallySmall_iff C).2 ⟨small_of_surjective Quotient.exists_rep, by infer_instance⟩

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