isStrictSegal

Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Nerve.isStrictSegal

English

The nerve of any category is a StrictSegal simplicial set.

Русский

Нерв категория является строгой сегаловой симплициальной множеством.

LaTeX

$$$$ \text{Nerve}(\mathcal{C}) \text{ is StrictSegal} $$$$

Lean4

instance isStrictSegal : IsStrictSegal (nerve C) :=
  strictSegal C |>.isStrictSegal

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

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

Разделы

Аффилиация

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