wellPowered

Mathlib.CategoryTheory.Generator.Basic

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

English

If HasPullbacks, Balanced, and HasSeparator, then WellPowered C.

Русский

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

LaTeX

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

Lean4

instance wellPowered [HasPullbacks C] [Balanced C] [HasSeparator C] : WellPowered.{v₁} C :=
  HasSeparator.hasDetector.wellPowered

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

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

Разделы

Аффилиация

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