isEquivalence

Mathlib.AlgebraicTopology.SimplexCategory.Basic

URI: https://scilib.ai/kg/mathlib#SimplexCategory.SkeletalFunctor.isEquivalence

English

SkeletalFunctor is an equivalence of categories, i.e., it is fully faithful and essentially surjective.

Русский

SkeletalFunctor — эквивалентность категорий: полно и верно полнообщее и существенно сюръективное.

LaTeX

$$$\\text{SkeletalFunctor isEquivalence}$$$

Lean4

noncomputable instance isEquivalence : skeletalFunctor.IsEquivalence where

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

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

Разделы

Аффилиация

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