reflectsLimitsOfShape_of_reflectsLimits

English

PreservesColimitsOfShape J by shape equivalence: preserves for shape J' if J ≃ J'.

Русский

Сохранение колимитов по форме J' через эквивалентность форм: сохранение для формы J' если J ≃ J'.

LaTeX

$$$ (e : J \\simeq J') \\ [PreservesColimitsOfShape J\\, F] \\Rightarrow PreservesColimitsOfShape J'\\, F. $$$

Lean4

instance (priority := 100) reflectsLimitsOfShape_of_reflectsLimits (J : Type w) [Category.{w'} J] (F : C ⥤ D)
    [ReflectsLimitsOfSize.{w', w} F] : ReflectsLimitsOfShape J F :=
  ReflectsLimitsOfSize.reflectsLimitsOfShape

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