colimitsOfShape_eq_of_equivalence

English

Same as above; invariance under equivalence of index shapes.

Русский

То же самое; инвариантность относительно эквивалентности индексов.

LaTeX

$$W.colimitsOfShape J = W.colimitsOfShape J'$$

Lean4

theorem colimitsOfShape_eq_of_equivalence {J' : Type*} [Category J'] (e : J ≌ J') :
    W.colimitsOfShape J = W.colimitsOfShape J' :=
  le_antisymm (W.colimitsOfShape_le_of_final e.inverse) (W.colimitsOfShape_le_of_final e.functor)

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