locallySmall — Mathlib

English

Let S: A ⥤ T be a functor, and X ∈ T; then CostructuredArrow S X is LocallySmall if A is LocallySmall.

Русский

Пусть S: A ⥤ T — функтор, и X ∈ T; CostructuredArrow S X локально мала, если A локально мала.

LaTeX

$$$\\\\operatorname{LocallySmall}(\\\\operatorname{CostructuredArrow} S X)$$$

Lean4

instance locallySmall (S : A ⥤ T) (X : T) [LocallySmall.{w} A] : LocallySmall.{w} (CostructuredArrow S X) :=
  Comma.locallySmall _ _

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