homMk₅_app_three

Mathlib.CategoryTheory.ComposableArrows

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

English

The component at index 5 of homMk5 equals app5.

Русский

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

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 ⟨5, by\; valid\rangle = app_5$$$

Lean4

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

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

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

Разделы

Аффилиация

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