homMk₂_app_one

Mathlib.CategoryTheory.ComposableArrows

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ComposableArrows.homMk₂_app_one

English

In the 2-length case, the component at index 1 of the morphism produced by homMk₂ equals the given app1.

Русский

В случае длины 2 компонент на позиции 1 создаваемого морфизма равен заданному app1.

LaTeX

$$$\\text{(homMk₂ app₀ app₁ app₂ w₀ w₁).app 1 = app₁}$$$

Lean4

@[simp]
theorem homMk₂_app_one : (homMk₂ app₀ app₁ app₂ w₀ w₁).app 1 = app₁ :=
  rfl

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

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

Разделы

Аффилиация

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