English
If C is locally small and well-powered and has finite limits, and T preserves finite limits, then the category of structured arrows S ⇒ T is well-powered.
Русский
Если C локально малое и хорошо порожденное, имеет конечные пределы и T сохраняет конечные пределы, то категория структурированных стрелок S ⇒ T является хорошо-порожденной.
LaTeX
$$$[\\text{LocallySmall } C] \\land [\\text{WellPowered } C] \\land [\\text{HasFiniteLimits } C] \\land [\\text{PreservesFiniteLimits } T]\\ \\Rightarrow\\ \\text{WellPowered}(\\mathrm{StructuredArrow}\; S\\; T).$$$
Lean4
/-- If `C` is well-powered and complete and `T` preserves limits, then `StructuredArrow S T` is
well-powered. -/
instance wellPowered_structuredArrow [LocallySmall.{w} C] [WellPowered.{w} C] [HasFiniteLimits C]
[PreservesFiniteLimits T] : WellPowered.{w} (StructuredArrow S T) where
subobject_small X := small_map (subobjectEquiv X).toEquiv
