wellPowered_of_isDetector — Mathlib

English

If G is a detector in a category with pullbacks, then the category is well-powered with respect to G; i.e., every object has a set of subobjects classified by G.

Русский

Если G является детектором в категории с вытягиванием, тогда категория хорошо снабжена подобъектами относительно G; то есть каждый объект имеет множество подобъектов, контролируемых G.

LaTeX

$$$\\text{HasPullbacks } C \\Rightarrow \\mathrm{WellPowered}(C)$ for IsDetector G$$

Lean4

theorem wellPowered_of_isDetector [HasPullbacks C] (G : C) (hG : IsDetector G) : WellPowered.{v₁} C :=
  wellPowered_of_isDetecting hG

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