inr_opProdIsoCoprod_inv

Mathlib.CategoryTheory.Limits.Opposites

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

← MathLib Explorer

English

coprod.inr ≫ (opProdIsoCoprod A B).inv = prod.snd.op

Русский

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

LaTeX

$$coprod.inr ≫ (opProdIsoCoprod A B).inv = prod.snd.op$$

Lean4

@[reassoc (attr := simp)]
theorem inr_opProdIsoCoprod_inv : coprod.inr ≫ (opProdIsoCoprod A B).inv = prod.snd.op := by
  rw [Iso.comp_inv_eq, snd_opProdIsoCoprod_hom]

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

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

Разделы

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

Аффилиация

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