mkNatTrans_app_right

Mathlib.CategoryTheory.Join.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Join.mkNatTrans_app_right

English

The right component of mkNatTrans αₗ αᵣ h at right d is αᵣ.app d.

Русский

Правая составляющая mkNatTrans αₗ αᵣ h на right d равна αᵣ.app d.

LaTeX

$$$ (\mathrm{mkNatTrans} αₗ αᵣ h).\mathrm{app}(\mathrm{right}\; d) = αᵣ.\mathrm{app} d $$$

Lean4

@[simp]
theorem mkNatTrans_app_right (d : D) : (mkNatTrans αₗ αᵣ h).app (right d) = αᵣ.app d :=
  rfl

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

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

Разделы

Аффилиация

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