instReflectsLimitWalkingParallelPairParallelPairOfIsCosplitPairOfReflectsLimitOfIsCosplitPair

English

There is an instance guaranteeing that if f,g form a cosplit pair, then PreservesLimit holds for the parallel pair with respect to F.

Русский

Существет экземпляр, гарантирующий, что если f,g образуют кослитную пару, то сохранение предела имеет место для параллельной пары относительно F.

LaTeX

$$$\operatorname{PreservesLimit}(\operatorname{parallelPair} f g) F,$ \\text{when } f,g \text{ are cosplit and } F \text{ preserves the limit.}$$$

Lean4

instance {A B} (f g : A ⟶ B) [F.IsCosplitPair f g] [ReflectsLimitOfIsCosplitPair F] :
    ReflectsLimit (parallelPair f g) F :=
  ReflectsLimitOfIsCosplitPair.out f g

Похожие утверждения