HomComplexInduction

📁 Source: Mathlib/Algebra/Homology/HomotopyCategory/HomComplexInduction.lean

Statistics

Metric	Count
Definitions EqUpTo, limitSequence, sequence	3
Theorems limitSequence_eqUpTo, sequence_eqUpTo	2
Total	5

CochainComplex.HomComplex.Cochain

Definitions

Name	Category	Theorems
EqUpTo 📖	MathDef	—

CochainComplex.HomComplex.Cochain.InductionUp

Definitions

Name	Category	Theorems
limitSequence 📖	CompOp	1 math math: limitSequence_eqUpTo
sequence 📖	CompOp	2 math math: limitSequence_eqUpTo, sequence_eqUpTo

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
limitSequence_eqUpTo 📖	mathematical	CochainComplex.HomComplex.Cochain.EqUpTo CochainComplex.HomComplex.Cochain Set Set.instMembership	limitSequence sequence	—	sequence_eqUpTo
sequence_eqUpTo 📖	mathematical	CochainComplex.HomComplex.Cochain.EqUpTo CochainComplex.HomComplex.Cochain Set Set.instMembership	sequence	—	AddRightCancelSemigroup.toIsRightCancelAdd

---

← Back to Index