Commit 2023-04-03 10:00 e00f1aa6

View on Github →

feat: port AlgebraicTopology.DoldKan.Compatibility (#3188)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicTopology/DoldKan/Compatibility.lean

added def AlgebraicTopology.DoldKan.Compatibility.equivalence

added theorem AlgebraicTopology.DoldKan.Compatibility.equivalence_functor

added def AlgebraicTopology.DoldKan.Compatibility.equivalence₀

added def AlgebraicTopology.DoldKan.Compatibility.equivalence₁

added def AlgebraicTopology.DoldKan.Compatibility.equivalence₁CounitIso

added theorem AlgebraicTopology.DoldKan.Compatibility.equivalence₁CounitIso_eq

added def AlgebraicTopology.DoldKan.Compatibility.equivalence₁UnitIso

added theorem AlgebraicTopology.DoldKan.Compatibility.equivalence₁UnitIso_eq

added theorem AlgebraicTopology.DoldKan.Compatibility.equivalence₁_inverse

added def AlgebraicTopology.DoldKan.Compatibility.equivalence₂

added def AlgebraicTopology.DoldKan.Compatibility.equivalence₂CounitIso

added theorem AlgebraicTopology.DoldKan.Compatibility.equivalence₂CounitIso_eq

added def AlgebraicTopology.DoldKan.Compatibility.equivalence₂UnitIso

added theorem AlgebraicTopology.DoldKan.Compatibility.equivalence₂UnitIso_eq

added theorem AlgebraicTopology.DoldKan.Compatibility.equivalence₂_inverse