Boundary

📁 Source: Mathlib/Algebra/Homology/Embedding/Boundary.lean

Statistics

Metric	Count
Definitions Boundary, BoundaryGE, BoundaryLE	3
Theorems false_of_isTruncLE, notMem, false_of_isTruncGE, notMem, boundaryGE, boundaryLE, next_f, next_f_of_not_boundaryLE, not_boundaryGE_next, not_boundaryGE_next', not_boundaryLE_prev, not_boundaryLE_prev', op_boundaryGE_iff, op_boundaryLE_iff, prev_f, prev_f_of_not_boundaryGE, boundaryGE_embeddingUpIntGE_iff, boundaryLE_embeddingUpIntLE_iff	18
Total	21

ComplexShape

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
boundaryGE_embeddingUpIntGE_iff 📖	mathematical	—	Embedding.BoundaryGE up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing embeddingUpIntGE	—	AddRightCancelSemigroup.toIsRightCancelAdd Nat.cast_zero add_zero CochainComplex.prev sub_add_cancel
boundaryLE_embeddingUpIntLE_iff 📖	mathematical	—	Embedding.BoundaryLE down AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne up AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing embeddingUpIntLE	—	AddRightCancelSemigroup.toIsRightCancelAdd Nat.cast_zero sub_zero CochainComplex.next

ComplexShape.Embedding

Definitions

Name	Category	Theorems
BoundaryGE 📖	MathDef	6 math math: AreComplementary.Boundary.snd, op_boundaryLE_iff, ComplexShape.boundaryGE_embeddingUpIntGE_iff, op_boundaryGE_iff, boundaryGE, not_boundaryGE_next
BoundaryLE 📖	MathDef	6 math math: AreComplementary.Boundary.fst, op_boundaryLE_iff, op_boundaryGE_iff, boundaryLE, not_boundaryLE_prev, ComplexShape.boundaryLE_embeddingUpIntLE_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
boundaryGE 📖	mathematical	ComplexShape.Rel f	BoundaryGE	—	ComplexShape.prev_eq'
boundaryLE 📖	mathematical	ComplexShape.Rel f	BoundaryLE	—	ComplexShape.next_eq'
next_f 📖	mathematical	ComplexShape.next	f	—	mem_next ComplexShape.next_eq' rel_iff IsTruncGE.toIsRelIff ComplexShape.next_eq_self
next_f_of_not_boundaryLE 📖	mathematical	ComplexShape.next BoundaryLE	f	—	ComplexShape.next_eq' rel_iff ComplexShape.next_eq_self
not_boundaryGE_next 📖	mathematical	ComplexShape.Rel	BoundaryGE	—	rel_iff
not_boundaryGE_next' 📖	—	BoundaryGE ComplexShape.next	—	—	not_boundaryGE_next ComplexShape.next_eq_self
not_boundaryLE_prev 📖	mathematical	ComplexShape.Rel	BoundaryLE	—	rel_iff
not_boundaryLE_prev' 📖	—	BoundaryLE ComplexShape.prev	—	—	not_boundaryLE_prev ComplexShape.prev_eq_self
op_boundaryGE_iff 📖	mathematical	—	BoundaryGE ComplexShape.symm op BoundaryLE	—	—
op_boundaryLE_iff 📖	mathematical	—	BoundaryLE ComplexShape.symm op BoundaryGE	—	—
prev_f 📖	mathematical	ComplexShape.prev	f	—	next_f instIsTruncGEOpOfIsTruncLE
prev_f_of_not_boundaryGE 📖	mathematical	ComplexShape.prev BoundaryGE	f	—	ComplexShape.prev_eq' rel_iff ComplexShape.prev_eq_self

ComplexShape.Embedding.AreComplementary

Definitions

Name	Category	Theorems
Boundary 📖	MathDef	4 math math: Boundary.of_boundaryGE, Boundary.exists₂, Boundary.of_boundaryLE, Boundary.exists₁

ComplexShape.Embedding.BoundaryGE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
false_of_isTruncLE 📖	—	ComplexShape.Embedding.BoundaryGE	—	—	ComplexShape.Embedding.mem_prev
notMem 📖	—	ComplexShape.Embedding.BoundaryGE ComplexShape.Rel ComplexShape.Embedding.f	—	—	—

ComplexShape.Embedding.BoundaryLE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
false_of_isTruncGE 📖	—	ComplexShape.Embedding.BoundaryLE	—	—	ComplexShape.Embedding.mem_next
notMem 📖	—	ComplexShape.Embedding.BoundaryLE ComplexShape.Rel ComplexShape.Embedding.f	—	—	—

---

← Back to Index