Commit 2023-04-19 14:33 bb39bf93

View on Github →

feat: port AlgebraicTopology.AlternatingFaceMapComplex (#3519)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean

added theorem AlgebraicTopology.AlternatingCofaceMapComplex.d_eq_unop_d

added theorem AlgebraicTopology.AlternatingCofaceMapComplex.d_squared

added def AlgebraicTopology.AlternatingCofaceMapComplex.map

added def AlgebraicTopology.AlternatingCofaceMapComplex.obj

added def AlgebraicTopology.AlternatingCofaceMapComplex.objD

added theorem AlgebraicTopology.AlternatingFaceMapComplex.d_squared

added def AlgebraicTopology.AlternatingFaceMapComplex.map

added theorem AlgebraicTopology.AlternatingFaceMapComplex.map_f

added def AlgebraicTopology.AlternatingFaceMapComplex.obj

added def AlgebraicTopology.AlternatingFaceMapComplex.objD

added theorem AlgebraicTopology.AlternatingFaceMapComplex.obj_X

added theorem AlgebraicTopology.AlternatingFaceMapComplex.obj_d_eq

added def AlgebraicTopology.AlternatingFaceMapComplex.ε

added def AlgebraicTopology.alternatingCofaceMapComplex

added def AlgebraicTopology.alternatingFaceMapComplex

added theorem AlgebraicTopology.alternatingFaceMapComplex_map_f

added theorem AlgebraicTopology.alternatingFaceMapComplex_obj_X

added theorem AlgebraicTopology.alternatingFaceMapComplex_obj_d

added def AlgebraicTopology.inclusionOfMooreComplex

added def AlgebraicTopology.inclusionOfMooreComplexMap

added theorem AlgebraicTopology.inclusionOfMooreComplexMap_f

added theorem AlgebraicTopology.karoubi_alternating_face_map_complex_d

added theorem AlgebraicTopology.map_alternatingFaceMapComplex