instIsEquivalenceIncl

Mathlib.CategoryTheory.FintypeCat

URI: https://scilib.ai/kg/mathlib#FintypeCat.Skeleton.instIsEquivalenceIncl

English

The inclusion of the skeleton into FintypeCat is an equivalence of categories.

Русский

Включение скелета в FintypeCat является эквивалентностью категорий.

LaTeX

$$$\\text{incl} : \\text{FintypeCat.Skeleton} \\to \\text{FintypeCat} \\text{ is an equivalence}$$$

Lean4

noncomputable instance : incl.IsEquivalence where

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

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

Разделы

Аффилиация

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