homMkSucc_app_zero

Mathlib.CategoryTheory.ComposableArrows

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

English

The first component of homMkSucc is α; the app at 0 is α.

Русский

Первая компонента HomMkSucc равна α; применённая к 0 даёт α.

LaTeX

$$$$ (homMkSucc\\ α\\ β\\ w).\\mathrm{app}\\ 0 = α $$$$

Lean4

@[simp]
theorem homMkSucc_app_zero : (homMkSucc α β w).app 0 = α :=
  rfl

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

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

Разделы

Аффилиация

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