instIsSerreClassTop

Mathlib.CategoryTheory.Abelian.SerreClass.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ObjectProperty.instIsSerreClassTop

English

The top object property provides an IsSerreClass instance; i.e., the entire category is a Serre class under that property.

Русский

Свойство верхнего объекта задаёт инстанс IsSerreClass; то есть вся категория образует Serre-подкатегорию.

LaTeX

$$$(\top : \text{ObjectProperty } C).IsSerreClass$$$

Lean4

instance : (⊤ : ObjectProperty C).IsSerreClass where

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

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

Разделы

Аффилиация

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