preservesLimitsOfShape_forget_of_isConnected

English

The forgetful functor forget B: Over B → C preserves any connected limit.

Русский

Ослабляющий функтор forget B: Over B → C сохраняет любой связанный предел.

LaTeX

$$$\text{PreservesLimitsOfShape}(\text{forget }B).$$$

Lean4

/-- The forgetful functor from the over category preserves any connected limit. -/
instance preservesLimitsOfShape_forget_of_isConnected [IsConnected J] {B : C} : PreservesLimitsOfShape J (forget B) :=
  inferInstanceAs <| PreservesLimitsOfShape J (CostructuredArrow.proj _ _)

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