homMk₂_app_two

Mathlib.CategoryTheory.ComposableArrows

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

English

In the 2-length case, the component at index 2 of homMk₂ is exactly app2.

Русский

В случае длины 2 компонент на позиции 2 в homMk₂ равен app2.

LaTeX

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

Lean4

@[simp]
theorem homMk₂_app_two : (homMk₂ app₀ app₁ app₂ w₀ w₁).app ⟨2, by valid⟩ = app₂ :=
  rfl

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

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

Разделы

Аффилиация

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