isInitialZero

Mathlib.CategoryTheory.Limits.Shapes.Preorder.Fin

URI: https://scilib.ai/kg/mathlib#Fin.isInitialZero

English

0 is an initial object in Fin n for n ≠ 0.

Русский

0 является начальным объектом в Fin n, когда n ≠ 0.

LaTeX

$$$[\text{NeZero } n] \Rightarrow (0: \mathrm{Fin} \, n) \text{ is initial}$$$

Lean4

/-- `0` is an initial object in `Fin n` when `n ≠ 0`. -/
def isInitialZero [NeZero n] : IsInitial (0 : Fin n) :=
  isInitialBot

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

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

Разделы

Аффилиация

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