inl_opProdIsoCoprod_inv

Mathlib.CategoryTheory.Limits.Opposites

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.inl_opProdIsoCoprod_inv

← MathLib Explorer

English

coprod.inl ≫ (opProdIsoCoprod A B).inv = prod.fst.op

Русский

coprod.inl после inverse(opProdIsoCoprod) равно prod.fst.op

LaTeX

$$coprod.inl ≫ (opProdIsoCoprod A B).inv = prod.fst.op$$

Lean4

@[reassoc (attr := simp)]
theorem inl_opProdIsoCoprod_inv : coprod.inl ≫ (opProdIsoCoprod A B).inv = prod.fst.op := by
  rw [Iso.comp_inv_eq, fst_opProdIsoCoprod_hom]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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