Theorems · Theorem · category theory
CochainComplex.isLE_iff
∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
(K : CochainComplex C ℤ) (n : ℤ), K.IsLE n ↔ ∀ (i : ℤ), n < i → HomologicalComplex.ExactAt K i- Cited by
- 3 results in Mathlib
- Foundations
- Depth 56 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- CategoryTheory.Limits.HasZeroMorphismsstatement and proof · cited by 3,275
- ComplexShape.upstatement · cited by 1,123
- CochainComplexstatement and proof · cited by 1,016
- ComplexShape.Embedding.fproof · cited by 251
- HomologicalComplex.ExactAtstatement and proof · cited by 44
- ComplexShape.embeddingUpIntLEproof · cited by 21
- CochainComplex.IsLEstatement and proof · cited by 11
- CochainComplex.exactAt_of_isLEproof · cited by 4
- ComplexShape.notMem_range_embeddingUpIntLE_iffproof · cited by 2
Cited by3
Results whose statement or proof uses this declaration.
- DerivedCategory.isLE_iffproof · cited by 1
- CochainComplex.isLE_of_leproof · cited by 0
- CochainComplex.isLE_shiftproof · cited by 0