hasFiniteProducts_of_has_binary_and_terminal

English

If a functor F preserves the terminal object and binary products, then it preserves all finite products.

Русский

Если функтор F сохраняет терминальный объект и бинарные произведения, он сохраняет все конечные произведения.

LaTeX

$$$$ \text{PreservesFiniteProducts.of_preserves_binary_and_terminal}(F) \;:\; \text{PreservesFiniteProducts } F. $$$$

Lean4

/-- If `C` has a terminal object and binary products, then it has finite products. -/
theorem hasFiniteProducts_of_has_binary_and_terminal : HasFiniteProducts C :=
  ⟨fun n =>
    ⟨fun K => by
      let that : (Discrete.functor fun n => K.obj ⟨n⟩) ≅ K := Discrete.natIso fun ⟨_⟩ => Iso.refl _
      rw [← hasLimit_iff_of_iso that]
      apply hasProduct_fin⟩⟩

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