Commit 2023-04-20 04:08 66fc2fe4

View on Github →

feat: port AlgebraicTopology.DoldKan.Homotopies (#3523)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicTopology/DoldKan/Homotopies.lean

added def AlgebraicTopology.DoldKan.Hσ

added theorem AlgebraicTopology.DoldKan.Hσ_eq_zero

added theorem AlgebraicTopology.DoldKan.c_mk

added theorem AlgebraicTopology.DoldKan.cs_down_0_not_rel_left

added def AlgebraicTopology.DoldKan.homotopyHσToZero

added def AlgebraicTopology.DoldKan.hσ'

added theorem AlgebraicTopology.DoldKan.hσ'_eq'

added theorem AlgebraicTopology.DoldKan.hσ'_eq

added theorem AlgebraicTopology.DoldKan.hσ'_eq_zero

added theorem AlgebraicTopology.DoldKan.hσ'_naturality

added def AlgebraicTopology.DoldKan.hσ

added theorem AlgebraicTopology.DoldKan.map_Hσ

added theorem AlgebraicTopology.DoldKan.map_hσ'

added def AlgebraicTopology.DoldKan.natTransHσ