homMk₅_app_two

Mathlib.CategoryTheory.ComposableArrows

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

English

The component at index 4 of homMk5 equals app4.

Русский

Компонент с индексом 4 в homMk5 равен app4.

LaTeX

$$$((homMk_5\; app_0\; app_1\; app_2\; app_3\; app_4\; app_5\; w_0\; w_1\; w_2\; w_3\; w_4).app ⟨4, by\; valid\rangle = app_4$$$

Lean4

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

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

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

Разделы

Аффилиация

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