OAI/Geometry/SingularHomology/HomologyHomotopyEquiv.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Problem340.realHomologyHomotopyEquivline 13 - theorem
OAI.Problem340.realHomologyHomotopyEquiv_applyline 36 - theorem
OAI.Problem340.realHomologyHomotopyEquiv_symm_applyline 40 - theorem
OAI.Problem340.realHomologyHomotopyEquiv_naturalityline 45 - abbrev
OAI.Problem340.realHomologyEquivOfHomotopyEquivline 56 - theorem
OAI.Problem340.realHomologyEquivOfHomotopyEquiv_applyline 59 - theorem
OAI.Problem340.realHomologyEquivOfHomotopyEquiv_symm_applyline 63