instIsLEObjCochainComplexIntQOfIsLE

English

For any cochain complex K of C with integer coefficients, if K satisfies the LE condition at n, then the associated object (Q.obj K) in the derived category also satisfies LE at n.

Русский

Для любого когомплекса K над C с коэффициентами в Z, если K удовлетворяет условию LE в уровне n, то связанный объект Q.obj K в производной категории также удовлетворяет LE в n.

LaTeX

$$$\forall (K : \text{CochainComplex } C \mathbb{Z}) (n : \mathbb{Z}), [K.IsLE\, n] \Rightarrow (Q.obj K).IsLE n$$$

Lean4

instance (K : CochainComplex C ℤ) (n : ℤ) [K.IsLE n] : (Q.obj K).IsLE n :=
  by
  rw [isLE_Q_obj_iff]
  infer_instance

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