prodIsoProd_inv_snd

Mathlib.Topology.Category.TopCat.Limits.Products

URI: https://scilib.ai/kg/mathlib#TopCat.prodIsoProd_inv_snd

← MathLib Explorer

English

Similarly, (prodIsoProd X Y).inv ≫ Limits.prod.snd = prodSnd.

Русский

Аналогично, (prodIsoProd X Y).inv ≫ Limits.prod.snd = prodSnd.

LaTeX

$$$(\\mathrm{prodIsoProd}(X,Y)).inv \\circ \\mathrm{Limits.prod.snd} = \\mathrm{prodSnd}$$$

Lean4

@[reassoc (attr := simp), elementwise]
theorem prodIsoProd_inv_snd (X Y : TopCat.{u}) : (prodIsoProd X Y).inv ≫ Limits.prod.snd = prodSnd := by
  simp [Iso.inv_comp_eq]

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

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

Разделы

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

Аффилиация

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