English
If F preserves finite products, then F preserves limits of shape of the discrete X-toTop carrier for finite X, i.e., limits over discrete diagrams on a finite carrier are preserved.
Русский
Если F сохраняет конечные произведения, то F сохраняет пределы формообразования дискретного карнера на конечной носителе, то есть пределы по дискретным диаграммам сохраняются.
LaTeX
$$$\\forall X\\ [Finite\\ X.toTop.carrier],\\text{ PreservesLimitsOfShape}(\\text{Discrete }X.toTop.carrier)\\ F$$$
Lean4
noncomputable instance (X : Profinite) [Finite X] : PreservesLimitsOfShape (Discrete X) F :=
let X' := (Countable.toSmall.{0} X).equiv_small.choose
let e : X ≃ X' := (Countable.toSmall X).equiv_small.choose_spec.some
have : Finite X' := .of_equiv X e
preservesLimitsOfShape_of_equiv (Discrete.equivalence e.symm) F
