homMk₄_app_four

Mathlib.CategoryTheory.ComposableArrows

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ComposableArrows.homMk₄_app_four

English

There is an isomorphism f ≅ g between ComposableArrows C 4 given app0..app4 and w0..w3.

Русский

Существует изоморфизм f ≅ g между ComposableArrows C 4, заданный app0..app4 и w0..w3.

LaTeX

$$$\\text{isoMk}_4 : f \\cong g$$$

Lean4

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

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

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

Разделы

Аффилиация

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