δlast

Mathlib.CategoryTheory.ComposableArrows

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ComposableArrows.δlast

English

Abbrev for forgetting the first arrow in a length-(n+1) composable arrows.

Русский

Аббревиатура для забывания первой стрелы в последовательности длины (n+1).

LaTeX

$$$$ \\delta_{last}(F) := δ_{last}(F) $$$$

Lean4

/-- The `ComposableArrows C n` obtained by forgetting the first arrow. -/
abbrev δlast (F : ComposableArrows C (n + 1)) :=
  δlastFunctor.obj F

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

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

Разделы

Аффилиация

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