essentiallySmall_monoOver — Mathlib

English

For every X, MonoOver X is EssentiallySmall provided C is LocallySmall and WellPowered.

Русский

Для каждого X MonoOver X есть свойство EssentiallySmall при условии LocallySmall и WellPowered.

LaTeX

$$$\forall X,\text{EssentiallySmall}(\mathrm{MonoOver}(X)).$$$

Lean4

instance essentiallySmall_monoOver (X : C) : EssentiallySmall.{w} (MonoOver X) :=
  (essentiallySmall_monoOver_iff_small_subobject X).mpr (WellPowered.subobject_small X)

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