preservesFilteredColimits — Mathlib

English

Another articulation that flipping K1 and K2 and applying G.flip preserves two-variable limit preservation.

Русский

Еще одно утверждение, что разворот K1 и K2 и применение G.flip сохраняют сохранение пределов в две переменные.

LaTeX

$$$PreservesLimit₂ K_2 K_1 G.flip$$$

Lean4

instance (priority := 100) preservesFilteredColimits (F : C ⥤ D) [PreservesColimitsOfSize.{w, w'} F] :
    PreservesFilteredColimitsOfSize.{w, w'} F where preserves_filtered_colimits _ := inferInstance

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