essentiallySmall_iff_of_thin — Mathlib

English

For a thin category, EssentiallySmall C is equivalent to Small(Skeleton C).

Русский

Для тонкой категории C: SUщественно-малость эквивалентна тому, что Skeleton(C) мала.

LaTeX

$$$\text{EssentiallySmall}(C) \iff \text{Small}(\text{Skeleton}(C))$$$

Lean4

/-- A thin category is essentially small if and only if the underlying type of its skeleton is small.
-/
theorem essentiallySmall_iff_of_thin {C : Type u} [Category.{v} C] [Quiver.IsThin C] :
    EssentiallySmall.{w} C ↔ Small.{w} (Skeleton C) := by
  simp [essentiallySmall_iff, CategoryTheory.locallySmall_of_thin]

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