sum'_obj_inr

Mathlib.CategoryTheory.Sums.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.sum'_obj_inr

English

Similarly, the object of (F.sum' G) on inr b equals G.obj b.

Русский

Аналогично, образ (F.sum' G) на inr b равен G.obj b.

LaTeX

$$$$ (F.sum' G).obj (\mathrm{Sum.inr}_ A B . b) = G.obj b. $$$$

Lean4

@[simp]
theorem sum'_obj_inr (b : B) : (F.sum' G).obj (inr b) = (G.obj b) :=
  rfl

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

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

Разделы

Аффилиация

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