instIsStrictlyGEObjHomologicalComplexIntUpSingle

English

For any object A in C, the complex concentrated at A in degree n is strictly GE at n.

Русский

Для каждого объекта A в C когепо concentration в степени n является строго GE в n.

LaTeX

$$$ \\forall A:\\mathrm{Obj}(\\mathcal{C}),\\ IsStrictlyGE(((\\mathrm{single}\\, \\mathcal{C}(\\mathrm{ComplexShape.up} \\mathbb{Z})\\, n).\\mathrm{obj}A))\\ n$$$

Lean4

instance (A : C) (n : ℤ) : IsStrictlyGE ((single C (ComplexShape.up ℤ) n).obj A) n :=
  by
  rw [isStrictlyGE_iff]
  intro i hi
  exact isZero_single_obj_X _ _ _ _ (by cutsat)

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