instHasTotalIntObjUpCompShiftFunctor₂ShiftFunctor₁

English

The composition of shift functors in both directions preserves totality: shifting first in the second index then in the first yields a total object.

Русский

Сохранение полноты при композиции сдвигов по обоим направлениям: сначала смещаем по второму индексу, затем по первому — получаем полный объект.

LaTeX

$$HasTotal (up ℤ) of ((shiftFunctor2 C y) ⋙ (shiftFunctor1 C x)).obj K$$

Lean4

instance : ((shiftFunctor₂ C y ⋙ shiftFunctor₁ C x).obj K).HasTotal (up ℤ) :=
  by
  dsimp
  infer_instance

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