hasBinaryProducts_of_hasLimit_pair

English

If a category C has all limits for diagrams of the form pair X Y, then C has all binary products.

Русский

Если в категории C существуют пределы диаграмм пары X Y, то у C существуют двоичные произведения.

LaTeX

$$$\forall C\; [HasLimit (pair X Y)]\;\Rightarrow\; HasBinaryProducts C$$$

Lean4

/-- If `C` has all limits of diagrams `pair X Y`, then it has all binary products -/
theorem hasBinaryProducts_of_hasLimit_pair [∀ {X Y : C}, HasLimit (pair X Y)] : HasBinaryProducts C :=
  { has_limit := fun F => hasLimit_of_iso (diagramIsoPair F).symm }

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