hasBinaryProducts_of_hasTerminal_and_pullbacks

English

Any category with a terminal object and pullbacks has all binary products.

Русский

Любая категория, обладающая терминальным объектом и pullbacks, имеет все бинарные произведения.

LaTeX

$$$\\forall C:\\\\text{Category},\\ HasTerminal C\\ \\land\\ HasPullbacks C\\;\\Rightarrow\\ HasBinaryProducts C$$$

Lean4

/-- Any category with pullbacks and terminal object has binary products. -/
theorem hasBinaryProducts_of_hasTerminal_and_pullbacks [HasTerminal C] [HasPullbacks C] : HasBinaryProducts C :=
  { has_limit := fun F => HasLimit.mk (limitConeOfTerminalAndPullbacks F) }

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