wellPowered

Mathlib.CategoryTheory.Generator.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.HasDetector.wellPowered

English

If C has pullbacks and a detector, then C is WellPowered.

Русский

Если в C имеются взятые обратные пределы (pullbacks) и детектор, то C является хорошо-насыщенной.

LaTeX

$$$\mathrm{WellPowered}(C)$$$

Lean4

instance wellPowered [HasPullbacks C] [HasDetector C] : WellPowered.{v₁} C :=
  isDetector_detector C |> wellPowered_of_isDetector _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru