essentiallySmall_monoOver_iff_small_subobject

English

For each X, MonoOver X is EssentiallySmall iff Subobject X is Small.

Русский

Для каждого X MonoOver X является essentiallySmall тогда и только тогда, когда Subobject X есть Small.

LaTeX

$$$\forall X,\ EssentiallySmall(\mathrm{MonoOver}(X)) \iff \mathrm{Small}(\mathrm{Subobject}(X)).$$$

Lean4

theorem essentiallySmall_monoOver_iff_small_subobject (X : C) :
    EssentiallySmall.{w} (MonoOver X) ↔ Small.{w} (Subobject X) :=
  essentiallySmall_iff_of_thin

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