instFullSimplexCategoryInclusion

Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic

URI: https://scilib.ai/kg/mathlib#AugmentedSimplexCategory.instFullSimplexCategoryInclusion

English

The augmentation-inclusion of AugmentedSimplexCategory into the augmented framework is full.

Русский

Включение AugmentedSimplexCategory вAugmented контекст является полным.

LaTeX

$$$\text{AugmentedSimplexCategory.inclusion.Full}$$$

Lean4

instance : inclusion.Full :=
  inferInstanceAs WithInitial.incl.Full

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

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

Разделы

Аффилиация

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