instSmallQuot

Mathlib.Algebra.Category.Grp.Colimits

URI: https://scilib.ai/kg/mathlib#AddCommGrpCat.instSmallQuot

English

There is a Small instance for Quot F: if J is decidable and small, then Quot F is small. Precisely, Small (Quot F).

Русский

Существование малой инстанции для Quot F: если J разрешимо и малая, то Quot F малая. Точно: Small (Quot F).

LaTeX

$$$ \text{Small }(\mathrm{Quot} F)$$$

Lean4

instance [DecidableEq J] [Small.{w} J] : Small.{w} (Quot F) :=
  small_of_surjective (QuotientAddGroup.mk'_surjective _)

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

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

Разделы

Аффилиация

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