prodLeftIsoPullback

Mathlib.CategoryTheory.Limits.Constructions.Over.Products

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Over.prodLeftIsoPullback

Lean4

/-- The product of `Y` and `Z` in `Over X` is isomorpic to `Y ×ₓ Z`. -/
noncomputable def prodLeftIsoPullback : (Y ⨯ Z).left ≅ pullback Y.hom Z.hom :=
  (Over.isPullback_of_binaryFan_isLimit _ (prodIsProd Y Z)).isoPullback

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

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

Разделы

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

Аффилиация

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