instIsStrictlyLEObjHomologicalComplexIntUpSingle

English

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

Русский

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

LaTeX

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

Lean4

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

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