English
If prodComparison F A B is an isomorphism for all A, B then F preserves limits of shape Discrete (WalkingPair).
Русский
Если для всех объектов A, B верно, что prodComparison F A B — изоморфизм, то F сохраняет пределы формы Discrete (WalkingPair).
LaTeX
$$$(\forall A,B,\ IsIso(\mathrm{prodComparison}\ F\ A\ B)) \Rightarrow \mathrm{PreservesLimitsOfShape}(\mathrm{Discrete\ WalkingPair})\ F$$$
Lean4
/-- If `prodComparison F A B` is an isomorphism for all `A B` then `F` preserves limits of shape
`Discrete (WalkingPair)`. -/
theorem preservesLimitsOfShape_discrete_walkingPair_of_isIso_prodComparison [∀ A B, IsIso (prodComparison F A B)] :
PreservesLimitsOfShape (Discrete WalkingPair) F :=
by
constructor
intro K
refine @preservesLimit_of_iso_diagram _ _ _ _ _ _ _ _ _ (diagramIsoPair K).symm ?_
apply preservesLimit_pair_of_isIso_prodComparison
