wellPowered_of_isSeparator — Mathlib

English

If C has pullbacks and is balanced and G is a separator, then C is well-powered; i.e., objects have a set of subobjects classified by G.

Русский

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

LaTeX

$$$[HasPullbacks\\ C]\\; [Balanced\\ C] \\Rightarrow \\mathrm{WellPowered}(C)$$$

Lean4

theorem wellPowered_of_isSeparator [HasPullbacks C] [Balanced C] (G : C) (hG : IsSeparator G) : WellPowered.{v₁} C :=
  wellPowered_of_isDetecting hG.isDetector

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