instEnoughProjectives

Mathlib.Topology.Category.CompHaus.Projective

URI: https://scilib.ai/kg/mathlib#CompHaus.instEnoughProjectives

English

CompHaus has enough projectives: every object admits a projective presentation.

Русский

У CompHaus достаточно проективных объектов: каждый объект имеет проективное представление.

LaTeX

$$$\mathrm{EnoughProjectives}(\mathrm{CompHaus})$$$

Lean4

instance : EnoughProjectives CompHaus where presentation X := ⟨projectivePresentation X⟩

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

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

Разделы

Аффилиация

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