English
If F preserves the initial object and binary coproducts, then it preserves coproducts for any finite index set J.
Русский
Если F сохраняет начальный объект и бинарные копроизведения, то он сохраняет копроизведения для любого конечного множества индексов J.
LaTeX
$$$\forall J\,[Finite J]\,:\\ PreservesColimitsOfShape(Discrete J) F$$$
Lean4
/-- If `F` preserves the initial object and binary coproducts then it preserves finite products. -/
theorem preservesFiniteCoproductsOfPreservesBinaryAndInitial (J : Type*) [Finite J] :
PreservesColimitsOfShape (Discrete J) F :=
let ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin J
have := preservesShape_fin_of_preserves_binary_and_initial F n
preservesColimitsOfShape_of_equiv (Discrete.equivalence e).symm _
