Boundary

📁 Source: Mathlib/AlgebraicTopology/SimplicialSet/Boundary.lean

Statistics

Metric	Count
Definitions boundary, «term∂Δ[_]»	2
Theorems boundary_eq_iSup	1
Total	3

SSet

Definitions

Name	Category	Theorems
boundary 📖	CompOp	12 math math: PtSimplex.RelStruct.δ_castSucc_map, PtSimplex.RelStruct.δ_castSucc_map_assoc, PtSimplex.MulStruct.δ_succ_succ_map_assoc, PtSimplex.MulStruct.δ_succ_succ_map, PtSimplex.MulStruct.δ_succ_castSucc_map, PtSimplex.MulStruct.δ_castSucc_castSucc_map_assoc, modelCategoryQuillen.boundary_ι_mem_I, boundary_eq_iSup, PtSimplex.RelStruct.δ_succ_map, PtSimplex.MulStruct.δ_succ_castSucc_map_assoc, PtSimplex.RelStruct.δ_succ_map_assoc, PtSimplex.MulStruct.δ_castSucc_castSucc_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
boundary_eq_iSup 📖	mathematical	—	boundary iSup Subcomplex CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet largeCategory stdSimplex ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CategoryTheory.instCompleteLatticeSubfunctor Opposite CategoryTheory.Category.opposite stdSimplex.face Compl.compl Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype Finset.instSingleton	—	CategoryTheory.Subfunctor.ext Set.ext CategoryTheory.Subfunctor.iSup_obj

Simplicial

Definitions

Name	Category	Theorems
«term∂Δ[_]» 📖	CompOp	—

---

← Back to Index