homMkSucc_app_succ

Mathlib.CategoryTheory.ComposableArrows

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

English

Every F ∈ ComposableArrows C (n+1) arises as a precomposition F₀.precomp f₀ for some F₀ and f₀.

Русский

Любой F ∈ ComposableArrows C (n+1) является F₀.precomp f₀ для некоторых F₀ и f₀.

LaTeX

$$$$ \\exists F_0, X_0, f_0\\,\\text{ such that } F = F_0.precomp f_0 $$$$

Lean4

@[simp]
theorem homMkSucc_app_succ (i : ℕ) (hi : i + 1 < n + 1 + 1) : (homMkSucc α β w).app ⟨i + 1, hi⟩ = app' β i :=
  rfl

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

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

Разделы

Аффилиация

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