fiberBinaryProductEquiv — Mathlib

English

The fiber of the binary product is the product of the fibers.

Русский

Фибра бинарного произведения равна произведению фибр.

LaTeX

$$$\\mathrm{F.obj}(X \\times Y) \\simeq \\mathrm{F.obj}(X) \\times \\mathrm{F.obj}(Y)$$$

Lean4

/-- The fiber of the binary product is the binary product of the fibers. -/
noncomputable def fiberBinaryProductEquiv (X Y : C) : F.obj (X ⨯ Y) ≃ F.obj X × F.obj Y :=
  (PreservesLimitPair.iso (F ⋙ FintypeCat.incl) X Y ≪≫ Types.binaryProductIso (F.obj X) (F.obj Y)).toEquiv

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