OAI/Geometry/SingularHomology/SubdivisionQuasiIso.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem340.SubdivisionComparison.exists_cycle_representative line 13
2. theorem OAI.Problem340.SubdivisionComparison.map_cycle line 25
3. theorem OAI.Problem340.SubdivisionComparison.reflect_cycle line 31
4. theorem OAI.Problem340.SubdivisionComparison.class_map_eq_class line 39
5. theorem OAI.Problem340.SubdivisionComparison.homologyMap_bijective_of_eventual_range line 47
6. theorem OAI.Problem340.SubdivisionComparison.quasiIso_of_eventual_range line 103
7. theorem OAI.Problem340.SubdivisionComparison.quasiIso_of_homotopy_eventual_range line 124
8. theorem OAI.Problem340.SubdivisionComparison.intertwines_pow line 139
9. theorem OAI.Problem340.SubdivisionComparison.homologyMap_pow_eq_id line 148
10. theorem OAI.Problem340.SubdivisionComparison.quasiIso_of_eventual_iterate_range line 158