obj_eq_Fin

Mathlib.AlgebraicTopology.SimplexCategory.Basic

URI: https://scilib.ai/kg/mathlib#SimplexCategory.toCat.obj_eq_Fin

English

The object corresponding to n in SimplexCategory via toCat is Fin(n+1).

Русский

Объект, соответствующий натуральному числу n в SimplexCategory через toCat, равен Fin(n+1).

LaTeX

$$$\\mathrm{toCat.obj}(\\langle n \\rangle)=\\mathrm{Fin}(n+1).$$$

Lean4

theorem obj_eq_Fin (n : ℕ) : toCat.obj ⦋n⦌ = Fin (n + 1) :=
  rfl

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

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

Разделы

Аффилиация

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