English
If F reflects finite products for discrete shapes, then F reflects finite limits on discrete shapes.
Русский
Если F отражает конечные произведения для дискретных форм, то F отражает конечные пределы на дискретных формах.
LaTeX
$$ReflectsLimitsOfShape(Discrete J) F from ReflectsFiniteProducts F$$
Lean4
instance (priority := 100) (F : C ⥤ D) [ReflectsFiniteProducts F] (J : Type u) [Finite J] :
ReflectsLimitsOfShape (Discrete J) F :=
let ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin J
have := ReflectsFiniteProducts.reflects (F := F) n
reflectsLimitsOfShape_of_equiv (Discrete.equivalence e.symm)
_
-- This is a dangerous instance as it has unbound universe variables.
