English
If F preserves finite limits, then F preserves finite products.
Русский
Если F сохраняет конечные пределы, то F сохраняет конечные произведения.
LaTeX
$$PreservesFiniteProducts F from PreservesFiniteLimits F$$
Lean4
instance (priority := 100) (F : C ⥤ D) (J : Type u) [Finite J] [PreservesFiniteProducts F] :
PreservesLimitsOfShape (Discrete J) F :=
by
obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin J
have := PreservesFiniteProducts.preserves (F := F) n
exact preservesLimitsOfShape_of_equiv (Discrete.equivalence e.symm) F
